refactor(init/meta,tools): rename now tactic to done

It was pointed out that Coq already uses `now` for a different kind of tactic.
And `done` is more descriptive anyway.

library/init/meta/interactive.lean

@@ -241,7 +241,7 @@ Like `exact`, but takes a list of terms and checks that all goals
 are discharged after the tactic.
 -/
 meta def exacts : parse qexpr_list_or_texpr → tactic unit
-| [] := now
+| [] := done
 | (t :: ts) := exact t >> exacts ts
 
 private meta def get_locals : list name → tactic (list expr)

library/init/meta/mk_has_sizeof_instance.lean

@@ -53,7 +53,7 @@ do szs ← mk_sizeof use_default I_name F_name field_names 0,
    exact (mk_sum szs)
 
 private meta def for_each_has_sizeof_goal : bool → name → name → list (list name) → tactic unit
-| d I_name F_name [] := now <|> fail "mk_has_sizeof_instance failed, unexpected number of cases"
+| d I_name F_name [] := done <|> fail "mk_has_sizeof_instance failed, unexpected number of cases"
 | d I_name F_name (ns::nss) := do
   solve1 (has_sizeof_case d I_name F_name ns),
   for_each_has_sizeof_goal d I_name F_name nss

library/init/meta/mk_inhabited_instance.lean

@@ -32,7 +32,7 @@ do tgt  ← target,
 private meta def try_constructors : nat → nat → tactic unit
 | 0     n := failed
 | (i+1) n :=
-  do {constructor_idx (n - i), all_goals mk_inhabited_arg, now}
+  do {constructor_idx (n - i), all_goals mk_inhabited_arg, done}
   <|>
   try_constructors i n
 

library/init/meta/smt/rsimp.lean

@@ -124,7 +124,7 @@ do focus1 $ using_smt_with {em_attr := cfg.attr_name} $
      add_lemmas_from_facts,
      add_lemmas extra,
      repeat_at_most cfg.max_rounds (ematch >> try smt_tactic.close),
-     (now >> return cc_state.mk)
+     (done >> return cc_state.mk)
      <|>
      to_cc_state
 

library/init/meta/tactic.lean

@@ -739,9 +739,9 @@ do n ← num_goals,
    when (n = 0) (fail "tactic failed, there are no goals to be solved")
 
 /- Fail if there are unsolved goals. -/
-meta def now : tactic unit :=
+meta def done : tactic unit :=
 do n ← num_goals,
-   when (n ≠ 0) (fail "now tactic failed, there are unsolved goals")
+   when (n ≠ 0) (fail "done tactic failed, there are unsolved goals")
 
 meta def apply (e : expr) : tactic unit :=
 apply_core e >> return ()

library/tools/mini_crush/default.lean

@@ -92,7 +92,7 @@ local_context >>= mfoldl (λ r h, mcond (is_inductive h) (return $ h::r) (return
 
 meta def try_induction_aux (cont : expr → tactic unit) : list expr → tactic unit
 | []      := failed
-| (e::es) := (step (induction e); cont e; now) <|> try_induction_aux es
+| (e::es) := (step (induction e); cont e; done) <|> try_induction_aux es
 
 meta def try_induction (cont : expr → tactic unit) : tactic unit :=
 focus1 $ collect_inductive_hyps >>= try_induction_aux cont
@@ -113,10 +113,10 @@ when_tracing `mini_crush $
 /- Simple tactic -/
 meta def close_aux (hs : hinst_lemmas) : tactic unit :=
     triv           <|> reflexivity reducible <|> contradiction
-<|> try_for 1000 (rsimp {} hs >> now) <|> try_for 1000 reflexivity
+<|> try_for 1000 (rsimp {} hs >> done) <|> try_for 1000 reflexivity
 
 meta def close (hs : hinst_lemmas) (s : name) (e : option expr) : tactic unit :=
-    now
+    done
 <|> close_aux hs
 <|> report_failure s e >> failed
 
@@ -135,11 +135,11 @@ tactic.write
 
 meta def try_snapshots {α} (cont : α → tactic unit) : list (α × snapshot) → tactic unit
 | []           := failed
-| ((a, s)::ss) := (restore s >> cont a >> now) <|> try_snapshots ss
+| ((a, s)::ss) := (restore s >> cont a >> done) <|> try_snapshots ss
 
 meta def search {α} (max_depth : nat) (act : nat → α → tactic (list (α × snapshot))) : nat → α → tactic unit
 | n s := do
-  now
+  done
   <|>
   if n > max_depth then when_tracing `mini_crush (trace "max depth reached" >> trace_state) >> failed
   else all_goals $ try intros >> act n s >>= try_snapshots (search (n+1))
@@ -208,7 +208,7 @@ meta def strategy_2_aux (cfg : simp_config) (hs : hinst_lemmas) : simp_lemmas
   do s ← simp_intro_aux cfg tt s tt [`_], -- Introduce next hypothesis
      h ← list.ilast <$> local_context,
      try $ solve1 (mwhen (is_inductive h) $ induction' h; simple s hs cfg "strategy 2" (some h)),
-     now <|> strategy_2_aux s
+     done <|> strategy_2_aux s
 
 meta def strategy_2 (cfg : simp_config := {}) (s : option simp_lemmas := none) (hs : option hinst_lemmas := none) : tactic unit :=
 do s ← mk_simp_lemmas s,
@@ -218,7 +218,7 @@ do s ← mk_simp_lemmas s,
 meta def strategy_3 (cfg : simp_config := {}) (max_depth : nat := 1) (s : option simp_lemmas := none) (hs : option hinst_lemmas := none) : tactic unit :=
 do s ← mk_simp_lemmas s,
    hs ← mk_hinst_lemmas hs,
-   try_induction (λ h, try (simph_intros_using s cfg); try (close_aux hs); (now <|> search_cases max_depth s hs cfg "strategy 3"))
+   try_induction (λ h, try (simph_intros_using s cfg); try (close_aux hs); (done <|> search_cases max_depth s hs cfg "strategy 3"))
 
 end mini_crush
 

library/tools/mini_crush/nano_crush.lean

@@ -90,7 +90,7 @@ local_context >>= mfoldl (λ r h, mcond (is_inductive h) (return $ h::r) (return
 
 meta def try_list_aux {α} (s : tactic_state) (tac : α → tactic unit) : list α → tactic unit
 | []      := failed
-| (e::es) := (write s >> tac e >> now) <|> try_list_aux es
+| (e::es) := (write s >> tac e >> done) <|> try_list_aux es
 
 meta def try_list {α} (tac : α → tactic unit) (es : list α) : tactic unit :=
 do s ← read, try_list_aux s tac es
@@ -102,8 +102,8 @@ meta def split (tac : tactic unit) : tactic unit :=
 collect_inductive_from_target >>= try_list (λ e, cases e; tac)
 
 meta def search (tac : tactic unit) : nat → tactic unit
-| 0     := all_goals tac >> now
-| (d+1) := all_goals (try tac) >> (now <|> split (search d))
+| 0     := all_goals tac >> done
+| (d+1) := all_goals (try tac) >> (done <|> split (search d))
 
 meta def rsimp' (hs : hinst_lemmas) : tactic unit :=
 rsimp {} hs

library/tools/super/cdcl_solver.lean

@@ -419,7 +419,7 @@ subgoal ← mk_meta_var s.local_false,
 goals ← get_goals,
 set_goals [subgoal],
 hvs ← for hyps (λhyp, assertv hyp.local_pp_name hyp.local_type hyp),
-solved ← (do th_solver, now, return tt) <|> return ff,
+solved ← (do th_solver, done, return tt) <|> return ff,
 set_goals goals,
 if solved then do
 proof ← instantiate_mvars subgoal,

library/tools/super/trim.lean

@@ -46,7 +46,7 @@ match gs with
   g' ← infer_type g >>= mk_meta_var,
   set_goals [g'],
   r ← tac,
-  now,
+  done,
   set_goals (g::gs),
   instantiate_mvars g' >>= trim' >>= exact,
   return r

tests/lean/run/aexp.lean

@@ -53,7 +53,7 @@ attribute [ematch] asimp_const aval
 
 -- set_option trace.smt.ematch true
 
-meta def not_done : tactic unit := fail_if_success now
+meta def not_done : tactic unit := fail_if_success done
 
 lemma aval_asimp_const (a : aexp) (s : state) : aval (asimp_const a) s = aval a s :=
 begin [smt]

tests/lean/run/listex3.lean

@@ -20,7 +20,7 @@ when_tracing `search_mem_list (do t ← target, f ← pp t, trace (to_fmt "searc
     (`[apply in_head])
     <|>
     (`[apply in_tail] >> mk_mem_list_rec))
->> now
+>> done
 
 meta def mk_mem_list : tactic unit :=
 solve1 mk_mem_list_rec