From 2ddc9d12bd4616f10245c40bc0c87ae548911809 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Apr 2017 19:13:58 +0200
Subject: Fixing #5420 as well as many related bugs due to miscounting let-ins.

- Supporting let-ins in tactic "fix", and hence in interactive
  Fixpoint and mutual theorems.
- Documenting more precisely the meaning of n in tactic "fix id n".
- Fixing computation of recursive index at interpretation time in the
  presence of let-ins.
---
 tactics/tactics.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0aab773140..43fc1d5111 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -507,6 +507,9 @@ let rec check_mutind env sigma k cl = match kind_of_term (strip_outer_cast cl) w
   else
     let open Context.Rel.Declaration in
     check_mutind (push_rel (LocalAssum (na, c1)) env) sigma (pred k) b
+| LetIn (na, c1, t, b) ->
+    let open Context.Rel.Declaration in
+    check_mutind (push_rel (LocalDef (na, c1, t)) env) sigma k b
 | _ -> error "Not enough products."
 
 (* Refine as a fixpoint *)
-- 
cgit v1.2.3


From 552544a3d385a3a59def038bdb0a22a69fe4b0a9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 7 Mar 2017 16:42:24 +0100
Subject: Removing the tclNOTSAMEGOAL primitive from the API.

The only use in Equality is reimplemented in the new engine.
---
 tactics/equality.ml   | 22 +++++++++++++++++++---
 tactics/tacticals.ml  |  1 -
 tactics/tacticals.mli |  1 -
 3 files changed, 19 insertions(+), 5 deletions(-)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7ae7446c82..e68be91e9b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -97,9 +97,6 @@ let _ =
 
 (* Rewriting tactics *)
 
-let tclNOTSAMEGOAL tac =
-  Proofview.V82.tactic (Tacticals.tclNOTSAMEGOAL (Proofview.V82.of_tactic tac))
-
 type dep_proof_flag = bool (* true = support rewriting dependent proofs *)
 type freeze_evars_flag = bool (* true = don't instantiate existing evars *)
 
@@ -268,6 +265,25 @@ let rewrite_elim with_evars frzevars cls c e =
   general_elim_clause with_evars flags cls c e
   end }
 
+let tclNOTSAMEGOAL tac =
+  let goal gl = Proofview.Goal.goal (Proofview.Goal.assume gl) in
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
+    let sigma = project gl in
+    let ev = goal gl in
+    tac >>= fun () ->
+    Proofview.Goal.goals >>= fun gls ->
+    let check accu gl' =
+      gl' >>= fun gl' ->
+      let accu = accu || Goal.V82.same_goal sigma ev (project gl') (goal gl') in
+      Proofview.tclUNIT accu
+    in
+    Proofview.Monad.List.fold_left check false gls >>= fun has_same ->
+    if has_same then
+      tclZEROMSG (str"Tactic generated a subgoal identical to the original goal.")
+    else
+      Proofview.tclUNIT ()
+  end }
+
 (* Ad hoc asymmetric general_elim_clause *)
 let general_elim_clause with_evars frzevars cls rew elim =
   let open Pretype_errors in
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 90b7d6581a..97922a4fa5 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -54,7 +54,6 @@ let tclDO            = Refiner.tclDO
 let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS
 let tclPROGRESS      = Refiner.tclPROGRESS
 let tclSHOWHYPS      = Refiner.tclSHOWHYPS
-let tclNOTSAMEGOAL   = Refiner.tclNOTSAMEGOAL
 let tclTHENTRY       = Refiner.tclTHENTRY
 let tclIFTHENELSE    = Refiner.tclIFTHENELSE
 let tclIFTHENSELSE   = Refiner.tclIFTHENSELSE
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 3b90ec514a..33933924ab 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -47,7 +47,6 @@ val tclDO            : int -> tactic -> tactic
 val tclWEAK_PROGRESS : tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclSHOWHYPS      : tactic -> tactic
-val tclNOTSAMEGOAL   : tactic -> tactic
 val tclTHENTRY       : tactic -> tactic -> tactic
 val tclMAP           : ('a -> tactic) -> 'a list -> tactic
 
-- 
cgit v1.2.3


From 21ee9a82807176acecf917e2a1e6074bed1c88ff Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 7 Mar 2017 18:16:27 +0100
Subject: Removing the tclWEAK_PROGRESS tactical.

The only remaining use was applied on the unfold tactic, and the behaviours
of tclPROGRESS and tclWEAK_PROGRESS coincide whenever only one goal is produced
by their argument tactic.
---
 tactics/class_tactics.ml | 3 +--
 tactics/tacticals.ml     | 1 -
 tactics/tacticals.mli    | 1 -
 3 files changed, 1 insertion(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index df222eed80..d70275dee5 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -462,8 +462,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
                    else e_trivial_fail_db only_classes db_list local_db secvars in
          Tacticals.New.tclTHEN fst snd
       | Unfold_nth c ->
-         let tac = Proofview.V82.of_tactic (unfold_in_concl [AllOccurrences,c]) in
-         Proofview.V82.tactic (tclWEAK_PROGRESS tac)
+         Proofview.tclPROGRESS (unfold_in_concl [AllOccurrences,c])
       | Extern tacast -> conclPattern concl p tacast
       in
       let tac = run_hint t tac in
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 97922a4fa5..5c97f27bab 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -51,7 +51,6 @@ let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE
 let tclFAIL          = Refiner.tclFAIL
 let tclFAIL_lazy     = Refiner.tclFAIL_lazy
 let tclDO            = Refiner.tclDO
-let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS
 let tclPROGRESS      = Refiner.tclPROGRESS
 let tclSHOWHYPS      = Refiner.tclSHOWHYPS
 let tclTHENTRY       = Refiner.tclTHENTRY
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 33933924ab..01b9e5e936 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -44,7 +44,6 @@ val tclAT_LEAST_ONCE : tactic -> tactic
 val tclFAIL          : int -> std_ppcmds -> tactic
 val tclFAIL_lazy     : int -> std_ppcmds Lazy.t -> tactic
 val tclDO            : int -> tactic -> tactic
-val tclWEAK_PROGRESS : tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclSHOWHYPS      : tactic -> tactic
 val tclTHENTRY       : tactic -> tactic -> tactic
-- 
cgit v1.2.3


From 81c964cfd9d7d3c4ea146889a59cc332987be03c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 7 Mar 2017 20:01:08 +0100
Subject: Porting generalize_dep to the new tactic engine.

---
 tactics/tactics.ml | 39 ++++++++++++++++++---------------------
 1 file changed, 18 insertions(+), 21 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e792585822..1615aec89a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2811,20 +2811,18 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl =
   mkProd_or_LetIn decl cl', sigma'
 
 let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) =
-  let env = Tacmach.pf_env gl in
-  let ids = Tacmach.pf_ids_of_hyps gl in
-  let sigma, t = Typing.type_of env sigma c in
-  generalize_goal_gen env sigma ids i o t cl
-
-let new_generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) =
-  let env = Tacmach.New.pf_env gl in
-  let ids = Tacmach.New.pf_ids_of_hyps gl in
+  let open Tacmach.New in
+  let env = pf_env gl in
+  let ids = pf_ids_of_hyps gl in
   let sigma, t = Typing.type_of env sigma c in
   generalize_goal_gen env sigma ids i o t cl
 
-let old_generalize_dep ?(with_let=false) c gl =
+let generalize_dep ?(with_let=false) c =
+  let open Tacmach.New in
+  let open Tacticals.New in
+  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
   let env = pf_env gl in
-  let sign = pf_hyps gl in
+  let sign = Proofview.Goal.hyps gl in
   let sigma = project gl in
   let init_ids = ids_of_named_context (Global.named_context()) in
   let seek (d:named_declaration) (toquant:named_context) =
@@ -2843,11 +2841,11 @@ let old_generalize_dep ?(with_let=false) c gl =
 	  -> id::tothin
       | _ -> tothin
   in
-  let cl' = it_mkNamedProd_or_LetIn (Tacmach.pf_concl gl) to_quantify in
+  let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in
   let body =
     if with_let then
       match EConstr.kind sigma c with
-      | Var id -> id |> Tacmach.pf_get_hyp gl |> NamedDecl.get_value
+      | Var id -> id |> (fun id -> pf_get_hyp id gl) |> NamedDecl.get_value
       | _ -> None
     else None
   in
@@ -2856,20 +2854,19 @@ let old_generalize_dep ?(with_let=false) c gl =
   (** Check that the generalization is indeed well-typed *)
   let (evd, _) = Typing.type_of env evd cl'' in
   let args = Context.Named.to_instance mkVar to_quantify_rev in
-  tclTHENLIST
-    [tclEVARS evd;
-     Proofview.V82.of_tactic (apply_type cl'' (if Option.is_empty body then c::args else args));
-     Proofview.V82.of_tactic (clear (List.rev tothin'))]
-    gl
-
-let generalize_dep ?(with_let = false) c =
-  Proofview.V82.tactic (old_generalize_dep ~with_let c)
+  let tac =
+    tclTHEN
+      (apply_type cl'' (if Option.is_empty body then c::args else args))
+      (clear (List.rev tothin'))
+  in
+  Sigma.Unsafe.of_pair (tac, evd)
+  end }
 
 (**  *)
 let generalize_gen_let lconstr = Proofview.Goal.s_enter { s_enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let newcl, evd =
-    List.fold_right_i (new_generalize_goal gl) 0 lconstr
+    List.fold_right_i (generalize_goal gl) 0 lconstr
       (Tacmach.New.pf_concl gl,Tacmach.New.project gl)
   in
   let (evd, _) = Typing.type_of env evd newcl in
-- 
cgit v1.2.3


From d272cd02ef9ba2509c266f58ee39f51106ae53c2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 11 Apr 2017 14:27:24 +0200
Subject: Fix the API of the new pf_constr_of_global.

The current implementation was still using continuation passing-style, and
furthermore was triggering a focus on the goals. We take advantage of the
tactic features instead.
---
 tactics/equality.ml   |  6 +++---
 tactics/tacticals.ml  | 14 ++++++--------
 tactics/tacticals.mli |  2 +-
 tactics/tactics.ml    |  6 +++---
 4 files changed, 13 insertions(+), 15 deletions(-)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index e68be91e9b..25c28cf4ac 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -658,8 +658,8 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
   | Some evd ->
     let e = build_coq_eq () in
     let sym = build_coq_eq_sym () in
-    Tacticals.New.pf_constr_of_global sym (fun sym ->
-    Tacticals.New.pf_constr_of_global e (fun e ->
+    Tacticals.New.pf_constr_of_global sym >>= fun sym ->
+    Tacticals.New.pf_constr_of_global e >>= fun e ->
     let eq = applist (e, [t1;c1;c2]) in
     tclTHENLAST
       (replace_core clause l2r eq)
@@ -667,7 +667,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
          [assumption;
           tclTHEN (apply sym) assumption;
           try_prove_eq
-         ])))
+         ])
   end }
 
 let replace c1 c2 =
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 5c97f27bab..c8441a8cc9 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -732,13 +732,11 @@ module New = struct
   let case_nodep_then_using =
     general_elim_then_using gl_make_case_nodep false
 
-  let pf_constr_of_global ref tac =
-    Proofview.Goal.enter { enter = begin fun gl ->
-      let env = Proofview.Goal.env gl in
-      let sigma = Tacmach.New.project gl in
-      let (sigma, c) = Evd.fresh_global env sigma ref in
-      let c = EConstr.of_constr c in
-      Proofview.Unsafe.tclEVARS sigma <*> (tac c)
-    end }
+  let pf_constr_of_global ref =
+    Proofview.tclEVARMAP >>= fun sigma ->
+    Proofview.tclENV >>= fun env ->
+    let (sigma, c) = Evd.fresh_global env sigma ref in
+    let c = EConstr.of_constr c in
+    Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT c
 
 end
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 01b9e5e936..5a4ecbac75 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -263,5 +263,5 @@ module New : sig
   val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args  -> unit Proofview.tactic
   val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args  -> unit Proofview.tactic
 
-  val pf_constr_of_global : Globnames.global_reference -> (constr -> unit Proofview.tactic) -> unit Proofview.tactic
+  val pf_constr_of_global : Globnames.global_reference -> constr Proofview.tactic
 end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1615aec89a..9c2a1d8509 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4721,7 +4721,7 @@ let symmetry_red allowred =
   | Some eq_data,_,_ ->
       Tacticals.New.tclTHEN
         (convert_concl_no_check concl DEFAULTcast)
-        (Tacticals.New.pf_constr_of_global eq_data.sym apply)
+        (Tacticals.New.pf_constr_of_global eq_data.sym >>= apply)
   | None,eq,eq_kind -> prove_symmetry eq eq_kind
   end }
 
@@ -4817,8 +4817,8 @@ let transitivity_red allowred t =
       Tacticals.New.tclTHEN
         (convert_concl_no_check concl DEFAULTcast)
         (match t with
-	  | None -> Tacticals.New.pf_constr_of_global eq_data.trans eapply
-	  | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans (fun trans -> apply_list [trans;t]))
+	  | None -> Tacticals.New.pf_constr_of_global eq_data.trans >>= eapply
+	  | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans >>= fun trans -> apply_list [trans; t])
    | None,eq,eq_kind ->
       match t with
       | None -> Tacticals.New.tclZEROMSG (str"etransitivity not supported for this relation.")
-- 
cgit v1.2.3


From 95b669a96f143d930b228a8b04041457040dd984 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 12 Apr 2017 13:48:36 +0200
Subject: Removing compatibility layer in Leminv.

---
 tactics/leminv.ml | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

(limited to 'tactics')

diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index daa962f1d6..83f3da30a9 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -260,22 +260,23 @@ let add_inversion_lemma_exn na com comsort bool tac =
 (* Applying a given inversion lemma  *)
 (* ================================= *)
 
-let lemInv id c gls =
+let lemInv id c =
+  Proofview.Goal.enter { enter = begin fun gls ->
   try
-    let open Tacmach in
     let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_unsafe_type_of gls c) in
     let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in
-    Proofview.V82.of_tactic (Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false) gls
+    Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false
   with
     | NoSuchBinding ->
 	user_err 
-	  (hov 0 (pr_econstr_env (Refiner.pf_env gls) (Refiner.project gls) c ++ spc () ++ str "does not refer to an inversion lemma."))
+	  (hov 0 (pr_econstr_env (pf_env gls) (project gls) c ++ spc () ++ str "does not refer to an inversion lemma."))
     | UserError (a,b) ->
 	 user_err ~hdr:"LemInv"
 	   (str "Cannot refine current goal with the lemma " ++
-	      pr_leconstr_env (Refiner.pf_env gls) (Refiner.project gls) c)
+	      pr_leconstr_env (pf_env gls) (project gls) c)
+  end }
 
-let lemInv_gen id c = try_intros_until (fun id -> Proofview.V82.tactic (lemInv id c)) id
+let lemInv_gen id c = try_intros_until (fun id -> lemInv id c) id
 
 let lemInvIn id c ids =
   Proofview.Goal.enter { enter = begin fun gl ->
@@ -289,7 +290,7 @@ let lemInvIn id c ids =
       else
         (tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids))
     in
-    ((tclTHEN (tclTHEN (bring_hyps hyps) (Proofview.V82.tactic (lemInv id c)))
+    ((tclTHEN (tclTHEN (bring_hyps hyps) (lemInv id c))
         (intros_replace_ids)))
   end }
 
-- 
cgit v1.2.3


From 98da9fdce866728f93bc7cb690275f5559aa9bae Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 16 Apr 2017 20:37:15 +0200
Subject: Removing various tactic compatibility layers in core tactics.

---
 tactics/auto.ml           | 11 ++++++-----
 tactics/class_tactics.ml  | 28 +++++++++++++++++-----------
 tactics/class_tactics.mli |  2 +-
 3 files changed, 24 insertions(+), 17 deletions(-)

(limited to 'tactics')

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 74cb7a364f..42230dff17 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -380,7 +380,7 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
 and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) =
   let tactic = function
     | Res_pf (c,cl) -> unify_resolve_gen poly flags (c,cl)
-    | ERes_pf _ -> Proofview.V82.tactic (fun gl -> error "eres_pf")
+    | ERes_pf _ -> Proofview.Goal.enter { enter = fun gl -> Tacticals.New.tclZEROMSG (str "eres_pf") }
     | Give_exact (c, cl)  -> exact poly (c, cl)
     | Res_pf_THEN_trivial_fail (c,cl) ->
       Tacticals.New.tclTHEN
@@ -389,10 +389,11 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=
 	   with "debug auto" we don't display the details of inner trivial *)
         (trivial_fail_db (no_dbg ()) (not (Option.is_empty flags)) db_list local_db)
     | Unfold_nth c ->
-      Proofview.V82.tactic (fun gl ->
-       if exists_evaluable_reference (pf_env gl) c then
-	 tclPROGRESS (Proofview.V82.of_tactic (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)) gl
-       else tclFAIL 0 (str"Unbound reference") gl)
+      Proofview.Goal.enter { enter = begin fun gl ->
+       if exists_evaluable_reference (Tacmach.New.pf_env gl) c then
+	 Tacticals.New.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)
+       else Tacticals.New.tclFAIL 0 (str"Unbound reference")
+       end }
     | Extern tacast -> 
       conclPattern concl p tacast
   in
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index d70275dee5..54e4405d1c 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -221,18 +221,22 @@ let auto_unif_flags freeze st =
     resolve_evars = false
 }
 
-let e_give_exact flags poly (c,clenv) gl =
+let e_give_exact flags poly (c,clenv) =
+  let open Tacmach.New in
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  let sigma = project gl in
   let (c, _, _) = c in
-  let c, gl =
+  let c, sigma =
     if poly then
       let clenv', subst = Clenv.refresh_undefined_univs clenv in
-      let evd = evars_reset_evd ~with_conv_pbs:true gl.sigma clenv'.evd in
+      let evd = evars_reset_evd ~with_conv_pbs:true sigma clenv'.evd in
       let c = Vars.subst_univs_level_constr subst c in
-        c, {gl with sigma = evd}
-    else c, gl
+        c, evd
+    else c, sigma
   in
-  let t1 = pf_unsafe_type_of gl c in
-  Proofview.V82.of_tactic (Clenvtac.unify ~flags t1 <*> exact_no_check c) gl
+  let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in
+  Sigma.Unsafe.of_pair (Clenvtac.unify ~flags t1 <*> exact_no_check c, sigma)
+  end }
 
 let unify_e_resolve poly flags = { enter = begin fun gls (c,_,clenv) ->
   let clenv', c = connect_hint_clenv poly c clenv gls in
@@ -455,7 +459,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
                    { enter = fun gl -> unify_resolve_refine poly flags gl (c,None,clenv) } in
              Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
-             Proofview.V82.tactic (e_give_exact flags poly (c,clenv))
+             e_give_exact flags poly (c,clenv)
       | Res_pf_THEN_trivial_fail (term,cl) ->
          let fst = with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in
          let snd = if complete then Tacticals.New.tclIDTAC
@@ -1613,9 +1617,11 @@ let not_evar c =
   | Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar")
   | _ -> Proofview.tclUNIT ()
 
-let is_ground c gl =
-  if Evarutil.is_ground_term (project gl) c then tclIDTAC gl
-  else tclFAIL 0 (str"Not ground") gl
+let is_ground c =
+  let open Tacticals.New in
+  Proofview.tclEVARMAP >>= fun sigma ->
+  if Evarutil.is_ground_term sigma c then tclIDTAC
+  else tclFAIL 0 (str"Not ground")
 
 let autoapply c i =
   let open Proofview.Notations in
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index a38be5972f..738cc0feba 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -33,7 +33,7 @@ val head_of_constr : Id.t -> constr -> unit Proofview.tactic
 
 val not_evar : constr -> unit Proofview.tactic
 
-val is_ground : constr -> tactic
+val is_ground : constr -> unit Proofview.tactic
 
 val autoapply : constr -> Hints.hint_db_name -> unit Proofview.tactic
 
-- 
cgit v1.2.3


From 11aaa1fd8230a347f1dca1a0f349ea7c7f2768c3 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 10 Jun 2016 18:58:24 -0400
Subject: Add support for transparent abstract (no syntax)

This is a small change that allows a transparent version of tclABSTRACT.
Additionally, it factors the machinery of [abstract] through a
plugin-accessible function which allows alternate continuations (other
than exact_no_check.

It might be nice to factor it further, into a cache_term function that
caches a term, and a separate bit that calls cache_term with the result
of running the tactic.
---
 tactics/tactics.ml  | 28 ++++++++++++++++++----------
 tactics/tactics.mli |  4 +++-
 2 files changed, 21 insertions(+), 11 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e792585822..19627eb530 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4907,7 +4907,7 @@ let shrink_entry sign const =
   } in
   (const, args)
 
-let abstract_subproof id gk tac =
+let cache_term_by_tactic_then id gk ?(opaque=true) tac tacK =
   let open Tacticals.New in
   let open Tacmach.New in
   let open Proofview.Notations in
@@ -4957,8 +4957,8 @@ let abstract_subproof id gk tac =
     else (const, List.rev (Context.Named.to_instance Constr.mkVar sign))
   in
   let args = List.map EConstr.of_constr args in
-  let cd = Entries.DefinitionEntry const in
-  let decl = (cd, IsProof Lemma) in
+  let cd = Entries.DefinitionEntry { const with Entries.const_entry_opaque = opaque } in
+  let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in
   let cst () =
     (** do not compute the implicit arguments, it may be costly *)
     let () = Impargs.make_implicit_args false in
@@ -4976,18 +4976,21 @@ let abstract_subproof id gk tac =
     Entries.(snd (Future.force const.const_entry_body)) in
   let solve =
     Proofview.tclEFFECTS effs <*>
-    exact_no_check (applist (lem, args))
+    tacK lem args
   in
   let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in
   Sigma.Unsafe.of_pair (tac, evd)
   end }
 
+let abstract_subproof id gk tac ?(opaque=true) =
+  cache_term_by_tactic_then id gk ~opaque:opaque tac (fun lem args -> exact_no_check (applist (lem, args)))
+
 let anon_id = Id.of_string "anonymous"
 
-let tclABSTRACT name_op tac =
+let name_op_to_name name_op object_kind suffix =
   let open Proof_global in
-  let default_gk = (Global, false, Proof Theorem) in
-  let s, gk = match name_op with
+  let default_gk = (Global, false, object_kind) in
+  match name_op with
     | Some s ->
       (try let _, gk, _ = current_proof_statement () in s, gk
        with NoCurrentProof -> s, default_gk)
@@ -4995,9 +4998,14 @@ let tclABSTRACT name_op tac =
       let name, gk =
 	try let name, gk, _ = current_proof_statement () in name, gk
 	with NoCurrentProof -> anon_id, default_gk in
-      add_suffix name "_subproof", gk
-  in
-  abstract_subproof s gk tac
+      add_suffix name suffix, gk
+
+let tclABSTRACT ?(opaque=true) name_op tac =
+  let open Proof_global in
+  let s, gk = if opaque
+    then name_op_to_name name_op (Proof Theorem) "_subproof"
+    else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in
+  abstract_subproof s gk tac ~opaque:opaque
 
 let unify ?(state=full_transparent_state) x y =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index ba4a9706de..d206011eed 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -401,7 +401,9 @@ val generalize_dep  : ?with_let:bool (** Don't lose let bindings *) -> constr  -
 
 val unify           : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic
 
-val tclABSTRACT : Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
+val cache_term_by_tactic_then : Id.t -> Decl_kinds.goal_kind -> ?opaque:bool -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic
+
+val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
 
 val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic
 val specialize_eqs : Id.t -> unit Proofview.tactic
-- 
cgit v1.2.3


From 12f34b2ebfcbe958ba53b49399c3fcaf01f7a18c Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 11 Apr 2017 09:50:55 -0400
Subject: Generalize cache_term_by_tactic_then

This will allow a cache_term tactic that doesn't suffer from the
Not_found anomalies of abstract in typeclass resolution.
---
 tactics/tactics.ml  | 7 +++++--
 tactics/tactics.mli | 2 +-
 2 files changed, 6 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 19627eb530..20de56645f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4907,7 +4907,7 @@ let shrink_entry sign const =
   } in
   (const, args)
 
-let cache_term_by_tactic_then id gk ?(opaque=true) tac tacK =
+let cache_term_by_tactic_then id gk ?(opaque=true) ?(goal_type=None) tac tacK =
   let open Tacticals.New in
   let open Tacmach.New in
   let open Proofview.Notations in
@@ -4927,7 +4927,10 @@ let cache_term_by_tactic_then id gk ?(opaque=true) tac tacK =
 	else (Context.Named.add d s1,s2))
       global_sign (Context.Named.empty, empty_named_context_val) in
   let id = next_global_ident_away id (pf_ids_of_hyps gl) in
-  let concl = it_mkNamedProd_or_LetIn (Proofview.Goal.concl gl) sign in
+  let concl = match goal_type with
+              | None ->  Proofview.Goal.concl gl
+              | Some ty -> ty in
+  let concl = it_mkNamedProd_or_LetIn concl sign in
   let concl =
     try flush_and_check_evars !evdref concl
     with Uninstantiated_evar _ ->
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index d206011eed..082812c5a6 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -401,7 +401,7 @@ val generalize_dep  : ?with_let:bool (** Don't lose let bindings *) -> constr  -
 
 val unify           : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic
 
-val cache_term_by_tactic_then : Id.t -> Decl_kinds.goal_kind -> ?opaque:bool -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic
+val cache_term_by_tactic_then : Id.t -> Decl_kinds.goal_kind -> ?opaque:bool -> ?goal_type:(constr option) -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic
 
 val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
 
-- 
cgit v1.2.3


From b348a11ccc4913598b72e4ecbb58811bcccd7bfc Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 11 Apr 2017 12:34:07 -0400
Subject: Make opaque optional only for tclABSTRACT

Also move named arguments to the beginning of the functions.  As per
https://github.com/coq/coq/pull/201#discussion_r110928302
---
 tactics/tactics.ml  | 8 ++++----
 tactics/tactics.mli | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 20de56645f..8f791cdcfe 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4907,7 +4907,7 @@ let shrink_entry sign const =
   } in
   (const, args)
 
-let cache_term_by_tactic_then id gk ?(opaque=true) ?(goal_type=None) tac tacK =
+let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
   let open Tacticals.New in
   let open Tacmach.New in
   let open Proofview.Notations in
@@ -4985,8 +4985,8 @@ let cache_term_by_tactic_then id gk ?(opaque=true) ?(goal_type=None) tac tacK =
   Sigma.Unsafe.of_pair (tac, evd)
   end }
 
-let abstract_subproof id gk tac ?(opaque=true) =
-  cache_term_by_tactic_then id gk ~opaque:opaque tac (fun lem args -> exact_no_check (applist (lem, args)))
+let abstract_subproof ~opaque id gk tac =
+  cache_term_by_tactic_then ~opaque:opaque id gk tac (fun lem args -> exact_no_check (applist (lem, args)))
 
 let anon_id = Id.of_string "anonymous"
 
@@ -5008,7 +5008,7 @@ let tclABSTRACT ?(opaque=true) name_op tac =
   let s, gk = if opaque
     then name_op_to_name name_op (Proof Theorem) "_subproof"
     else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in
-  abstract_subproof s gk tac ~opaque:opaque
+  abstract_subproof ~opaque:opaque s gk tac
 
 let unify ?(state=full_transparent_state) x y =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 082812c5a6..07a8035427 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -401,7 +401,7 @@ val generalize_dep  : ?with_let:bool (** Don't lose let bindings *) -> constr  -
 
 val unify           : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic
 
-val cache_term_by_tactic_then : Id.t -> Decl_kinds.goal_kind -> ?opaque:bool -> ?goal_type:(constr option) -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic
+val cache_term_by_tactic_then : opaque:bool -> ?goal_type:(constr option) -> Id.t -> Decl_kinds.goal_kind -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic
 
 val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
 
-- 
cgit v1.2.3


From 1e046726dc9352f7979ebdeba0d750e44016fea5 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 11 Apr 2017 12:48:23 -0400
Subject: transparent abstract: Respond to review comment

https://github.com/coq/coq/pull/201#discussion_r110952601
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8f791cdcfe..d02fe86653 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4986,7 +4986,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
   end }
 
 let abstract_subproof ~opaque id gk tac =
-  cache_term_by_tactic_then ~opaque:opaque id gk tac (fun lem args -> exact_no_check (applist (lem, args)))
+  cache_term_by_tactic_then ~opaque id gk tac (fun lem args -> exact_no_check (applist (lem, args)))
 
 let anon_id = Id.of_string "anonymous"
 
-- 
cgit v1.2.3


From e4262a89d7bc3d9b985d9a4a939f34176581abcb Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 11 Apr 2017 13:05:54 -0400
Subject: transparent abstract: Respond to review comment

https://github.com/coq/coq/pull/201#discussion_r110957570
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d02fe86653..4654817035 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5008,7 +5008,7 @@ let tclABSTRACT ?(opaque=true) name_op tac =
   let s, gk = if opaque
     then name_op_to_name name_op (Proof Theorem) "_subproof"
     else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in
-  abstract_subproof ~opaque:opaque s gk tac
+  abstract_subproof ~opaque s gk tac
 
 let unify ?(state=full_transparent_state) x y =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
-- 
cgit v1.2.3


From 2826683746569b9d78aa01e319315ab554e1619b Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 19:36:45 +0200
Subject: Fix omitted labels in function calls

---
 tactics/class_tactics.ml | 6 +++---
 tactics/hints.ml         | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 54e4405d1c..c430e776a4 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -357,12 +357,12 @@ let shelve_dependencies gls =
 
 let hintmap_of sigma hdc secvars concl =
   match hdc with
-  | None -> fun db -> Hint_db.map_none secvars db
+  | None -> fun db -> Hint_db.map_none ~secvars db
   | Some hdc ->
      fun db ->
      if Hint_db.use_dn db then (* Using dnet *)
-       Hint_db.map_eauto sigma secvars hdc concl db
-     else Hint_db.map_existential sigma secvars hdc concl db
+       Hint_db.map_eauto sigma ~secvars hdc concl db
+     else Hint_db.map_existential sigma ~secvars hdc concl db
 
 (** Hack to properly solve dependent evars that are typeclasses *)
 let rec e_trivial_fail_db only_classes db_list local_db secvars =
diff --git a/tactics/hints.ml b/tactics/hints.ml
index bcc068d3da..240178c9a9 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1435,7 +1435,7 @@ let pr_hints_db (name,db,hintlist) =
 let pr_hint_list_for_head c =
   let dbs = current_db () in
   let validate (name, db) =
-    let hints = List.map (fun v -> 0, v) (Hint_db.map_all Id.Pred.full c db) in
+    let hints = List.map (fun v -> 0, v) (Hint_db.map_all ~secvars:Id.Pred.full c db) in
     (name, db, hints)
   in
   let valid_dbs = List.map validate dbs in
-- 
cgit v1.2.3


From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:04:58 +0200
Subject: Remove some unused values and types

---
 tactics/hipattern.ml | 1 -
 tactics/tactics.ml   | 2 --
 2 files changed, 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 851554b832..15b40b42d1 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -40,7 +40,6 @@ let mkmeta n = Nameops.make_ident "X" (Some n)
 let meta1 = mkmeta 1
 let meta2 = mkmeta 2
 let meta3 = mkmeta 3
-let meta4 = mkmeta 4
 
 let op2bool = function Some _ -> true | None -> false
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 9c2a1d8509..53f8e4d5fe 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5039,8 +5039,6 @@ end
 module New = struct
   open Proofview.Notations
 
-  let exact_proof c = exact_proof c
-
   open Genredexpr
   open Locus
 
-- 
cgit v1.2.3


From 528c237b658dbba896a1fe0041990cc7fec9c4c8 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:07:32 +0200
Subject: Add [_] prefix to unused values which maybe should be kept

---
 tactics/term_dnet.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 2c863c42a6..726fd23b64 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -49,7 +49,7 @@ struct
     | DNil
 
   (* debug *)
-  let pr_dconstr f : 'a t -> std_ppcmds = function
+  let _pr_dconstr f : 'a t -> std_ppcmds = function
     | DRel -> str "*"
     | DSort -> str "Sort"
     | DRef _ -> str "Ref"
-- 
cgit v1.2.3


From 4e84e83911c1cf7613a35b921b1e68e097f84b5a Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:11:47 +0200
Subject: Remove unused [open] statements

---
 tactics/auto.ml           | 1 -
 tactics/auto.mli          | 1 -
 tactics/btermdn.mli       | 1 -
 tactics/class_tactics.ml  | 3 ---
 tactics/class_tactics.mli | 1 -
 tactics/contradiction.mli | 1 -
 tactics/eauto.mli         | 2 --
 tactics/elim.ml           | 1 -
 tactics/elim.mli          | 1 -
 tactics/eqdecide.ml       | 1 -
 tactics/equality.ml       | 1 -
 tactics/equality.mli      | 1 -
 tactics/hints.mli         | 1 -
 tactics/hipattern.mli     | 1 -
 tactics/inv.ml            | 1 -
 tactics/inv.mli           | 1 -
 tactics/leminv.mli        | 1 -
 tactics/tactics.ml        | 2 --
 18 files changed, 22 deletions(-)

(limited to 'tactics')

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 42230dff17..324c551d05 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -12,7 +12,6 @@ open Pp
 open Util
 open CErrors
 open Names
-open Vars
 open Termops
 open EConstr
 open Environ
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 32710e3470..9ed9f0ae26 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -9,7 +9,6 @@
 (** This files implements auto and related automation tactics *)
 
 open Names
-open Term
 open EConstr
 open Clenv
 open Pattern
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index 2a5e7c3458..27f624f716 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open Pattern
 open Names
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index c430e776a4..6c724a1eb1 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -18,7 +18,6 @@ open Names
 open Term
 open Termops
 open EConstr
-open Reduction
 open Proof_type
 open Tacticals
 open Tacmach
@@ -1219,7 +1218,6 @@ module Search = struct
 
   let intro_tac info kont gl =
     let open Proofview in
-    let open Proofview.Notations in
     let env = Goal.env gl in
     let sigma = Goal.sigma gl in
     let s = Sigma.to_evar_map sigma in
@@ -1257,7 +1255,6 @@ module Search = struct
   let search_tac_gl ?st only_classes dep hints depth i sigma gls gl :
         unit Proofview.tactic =
     let open Proofview in
-    let open Proofview.Notations in
     if false (* In 8.6, still allow non-class goals only_classes && not (is_class_type sigma (Goal.concl gl)) *) then
       Tacticals.New.tclZEROMSG (str"Not a subgoal for a class")
     else
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index 738cc0feba..4ab29f260f 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -9,7 +9,6 @@
 (** This files implements typeclasses eauto *)
 
 open Names
-open Constr
 open EConstr
 open Tacmach
 
diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli
index 510b135b0a..2cf5a68298 100644
--- a/tactics/contradiction.mli
+++ b/tactics/contradiction.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open EConstr
 open Misctypes
 
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index e2006ac1e3..c952f4e721 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -6,9 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open EConstr
-open Proof_type
 open Hints
 open Tactypes
 
diff --git a/tactics/elim.ml b/tactics/elim.ml
index e37ec6bce2..855cb206fe 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -8,7 +8,6 @@
 
 open Util
 open Names
-open Term
 open Termops
 open EConstr
 open Inductiveops
diff --git a/tactics/elim.mli b/tactics/elim.mli
index dc1af79ba0..fb7cc7b838 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open EConstr
 open Tacticals
 open Misctypes
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index bac3980d2b..5012b0ef7f 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -25,7 +25,6 @@ open Constr_matching
 open Misctypes
 open Tactypes
 open Hipattern
-open Pretyping
 open Proofview.Notations
 open Tacmach.New
 open Coqlib
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 25c28cf4ac..cc7701ad5f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -14,7 +14,6 @@ open Names
 open Nameops
 open Term
 open Termops
-open Environ
 open EConstr
 open Vars
 open Namegen
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 5467b4af25..d979c580aa 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -8,7 +8,6 @@
 
 (*i*)
 open Names
-open Term
 open Evd
 open EConstr
 open Environ
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 467fd46d53..3a0339ff57 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -9,7 +9,6 @@
 open Pp
 open Util
 open Names
-open Term
 open EConstr
 open Environ
 open Globnames
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index dd09c3a4d7..82a3d47b59 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open Evd
 open EConstr
 open Coqlib
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 904a17417a..266cac5c7d 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -13,7 +13,6 @@ open Names
 open Nameops
 open Term
 open Termops
-open Environ
 open EConstr
 open Vars
 open Namegen
diff --git a/tactics/inv.mli b/tactics/inv.mli
index 446a62f6db..5835e763dd 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open EConstr
 open Misctypes
 open Tactypes
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 26d4ac994b..a343fc81a7 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open EConstr
 open Constrexpr
 open Misctypes
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 53f8e4d5fe..f3f7d16b76 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5037,8 +5037,6 @@ end
 
 (** Tacticals defined directly in term of Proofview *)
 module New = struct
-  open Proofview.Notations
-
   open Genredexpr
   open Locus
 
-- 
cgit v1.2.3


From 9a48211ea8439a8502145e508b70ede9b5929b2f Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Thu, 27 Apr 2017 21:58:52 +0200
Subject: Post-rebase warnings (unused opens and 2 unused values)

---
 tactics/auto.ml           | 3 ---
 tactics/class_tactics.ml  | 1 -
 tactics/class_tactics.mli | 1 -
 3 files changed, 5 deletions(-)

(limited to 'tactics')

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 324c551d05..c2d12ebd08 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -10,15 +10,12 @@ module CVars = Vars
 
 open Pp
 open Util
-open CErrors
 open Names
 open Termops
 open EConstr
 open Environ
-open Tacmach
 open Genredexpr
 open Tactics
-open Tacticals
 open Clenv
 open Locus
 open Proofview.Notations
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 6c724a1eb1..2d6dffdd23 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -19,7 +19,6 @@ open Term
 open Termops
 open EConstr
 open Proof_type
-open Tacticals
 open Tacmach
 open Tactics
 open Clenv
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index 4ab29f260f..c5731e3779 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -10,7 +10,6 @@
 
 open Names
 open EConstr
-open Tacmach
 
 val catchable : exn -> bool
 
-- 
cgit v1.2.3


From 7943b1fade775af48917d54878e65b80217be038 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 28 Apr 2017 16:15:10 +0200
Subject: Using a more explicit algebraic type for evars of kind "MatchingVar".

A priori considered to be a good programming style.
---
 tactics/hipattern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 851554b832..257c092d72 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -261,7 +261,7 @@ let mkGProd id c1 c2 =
 let mkGArrow c1 c2 =
   GProd (Loc.ghost, Anonymous, Explicit, c1, c2)
 let mkGVar id = GVar (Loc.ghost, Id.of_string id)
-let mkGPatVar id = GPatVar(Loc.ghost, (false, Id.of_string id))
+let mkGPatVar id = GPatVar(Loc.ghost, Evar_kinds.FirstOrderPatVar (Id.of_string id))
 let mkGRef r = GRef (Loc.ghost, Lazy.force r, None)
 let mkGAppRef r args = mkGApp (mkGRef r) args
 
-- 
cgit v1.2.3


From 4f742e14441581ece247d33020055f15732f126b Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 28 Apr 2017 22:14:09 +0200
Subject: Revert "Using a more explicit algebraic type for evars of kind
 "MatchingVar"."

I'm sure this was pushed by accident, since testing shows immediately
that it breaks the compilation of the ssreflect plugin, hence all
developments relying on it in Travis.
---
 tactics/hipattern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 257c092d72..851554b832 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -261,7 +261,7 @@ let mkGProd id c1 c2 =
 let mkGArrow c1 c2 =
   GProd (Loc.ghost, Anonymous, Explicit, c1, c2)
 let mkGVar id = GVar (Loc.ghost, Id.of_string id)
-let mkGPatVar id = GPatVar(Loc.ghost, Evar_kinds.FirstOrderPatVar (Id.of_string id))
+let mkGPatVar id = GPatVar(Loc.ghost, (false, Id.of_string id))
 let mkGRef r = GRef (Loc.ghost, Lazy.force r, None)
 let mkGAppRef r args = mkGApp (mkGRef r) args
 
-- 
cgit v1.2.3


From edb21eab674b170d125a5b6fbc8213066b356d17 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 6 Apr 2017 10:10:03 +0200
Subject: Fixing "decide equality"'s bug #5449.

The code was assuming that the terms t and u for which {t=u}+{t<>u} is
proved were distinct. We refine an internal "generalize" of "u" so
that it works on the two precise occurrences to abstract, even if
other occurrences of u occur as subterm of t too.

We also reuse the global constants found in the statement rather than
reconstructing them (this seems better in case the global constants
eventually get polymorphic universes?).
---
 tactics/eqdecide.ml | 57 ++++++++++++++++++++++++++++++++++++++++++-----------
 1 file changed, 46 insertions(+), 11 deletions(-)

(limited to 'tactics')

diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index bac3980d2b..7d8b84f9c8 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -67,9 +67,27 @@ let choose_noteq eqonleft =
   else
     left_with_bindings false Misctypes.NoBindings
 
-let mkBranches c1 c2 =
+open Sigma.Notations
+open Context.Rel.Declaration
+
+(* A surgical generalize which selects the right occurrences by hand *)
+(* This prevents issues where c2 is also a subterm of c1 (see e.g. #5449) *)
+
+let generalize_right mk typ c1 c2 =
+  Proofview.Goal.enter { Proofview.Goal.enter = begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let store = Proofview.Goal.extra gl in
+  Refine.refine ~unsafe:true { Sigma.run = begin fun sigma ->
+    let na = Name (next_name_away_with_default "x" Anonymous (Termops.ids_of_context env)) in
+    let newconcl = mkProd (na, typ, mk typ c1 (mkRel 1)) in
+    let Sigma (x, sigma, p) = Evarutil.new_evar env sigma ~principal:true ~store newconcl in
+    Sigma (mkApp (x, [|c2|]), sigma, p)
+  end }
+  end }
+
+let mkBranches (eqonleft,mk,c1,c2,typ) =
   tclTHENLIST
-    [generalize [c2];
+    [generalize_right mk typ c1 c2;
      Simple.elim c1;
      intros;
      onLastHyp Simple.case;
@@ -145,15 +163,32 @@ let diseqCase hyps eqonleft =
 
 open Proofview.Notations
 
-(* spiwack: a small wrapper around [Hipattern]. *)
+(* spiwack: a PatternMatchingFailure wrapper around [Hipattern]. *)
 
 let match_eqdec sigma c =
-  try Proofview.tclUNIT (match_eqdec sigma c)
+  try
+    let (eqonleft,_,c1,c2,ty) = match_eqdec sigma c in
+    let (op,eq1,noteq,eq2) =
+      match EConstr.kind sigma c with
+      | App (op,[|ty1;ty2|]) ->
+         let ty1, ty2 = if eqonleft then ty1, ty2 else ty2, ty1 in
+         (match EConstr.kind sigma ty1, EConstr.kind sigma ty2 with
+         | App (eq1,_), App (noteq,[|neq|]) ->
+            (match EConstr.kind sigma neq with
+             | App (eq2,_) -> op,eq1,noteq,eq2
+             | _ -> assert false)
+         | _ -> assert false)
+      | _ -> assert false in
+    let mk t x y =
+      let eq = mkApp (eq1,[|t;x;y|]) in
+      let neq = mkApp (noteq,[|mkApp (eq2,[|t;x;y|])|]) in
+      if eqonleft then mkApp (op,[|eq;neq|]) else mkApp (op,[|neq;eq|]) in
+    Proofview.tclUNIT (eqonleft,mk,c1,c2,ty)
   with PatternMatchingFailure -> Proofview.tclZERO PatternMatchingFailure
 
 (* /spiwack *)
 
-let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with
+let rec solveArg hyps eqonleft mk largs rargs = match largs, rargs with
 | [], [] ->
   tclTHENLIST [
     choose_eq eqonleft;
@@ -163,8 +198,8 @@ let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with
 | a1 :: largs, a2 :: rargs ->
   Proofview.Goal.enter { enter = begin fun gl ->
   let rectype = pf_unsafe_type_of gl a1 in
-  let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in
-  let tac hyp = solveArg (hyp :: hyps) eqonleft op largs rargs in
+  let decide = mk rectype a1 a2 in
+  let tac hyp = solveArg (hyp :: hyps) eqonleft mk largs rargs in
   let subtacs =
     if eqonleft then [eqCase tac;diseqCase hyps eqonleft;default_auto]
     else [diseqCase hyps eqonleft;eqCase tac;default_auto] in
@@ -178,13 +213,13 @@ let solveEqBranch rectype =
       Proofview.Goal.enter { enter = begin fun gl ->
         let concl = pf_concl gl in
         let sigma = project gl in
-        match_eqdec sigma concl >>= fun (eqonleft,op,lhs,rhs,_) ->
+        match_eqdec sigma concl >>= fun (eqonleft,mk,lhs,rhs,_) ->
           let (mib,mip) = Global.lookup_inductive rectype in
           let nparams   = mib.mind_nparams in
           let getargs l = List.skipn nparams (snd (decompose_app sigma l)) in
           let rargs   = getargs rhs
           and largs   = getargs lhs in
-          solveArg [] eqonleft op largs rargs
+          solveArg [] eqonleft mk largs rargs
       end }
     end
     begin function (e, info) -> match e with
@@ -204,14 +239,14 @@ let decideGralEquality =
       Proofview.Goal.enter { enter = begin fun gl ->
         let concl = pf_concl gl in
         let sigma = project gl in
-        match_eqdec sigma concl >>= fun (eqonleft,_,c1,c2,typ) ->
+        match_eqdec sigma concl >>= fun (eqonleft,mk,c1,c2,typ as data) ->
         let headtyp = hd_app sigma (pf_compute gl typ) in
         begin match EConstr.kind sigma headtyp with
         | Ind (mi,_) -> Proofview.tclUNIT mi
         | _ -> tclZEROMSG (Pp.str"This decision procedure only works for inductive objects.")
         end >>= fun rectype ->
           (tclTHEN
-             (mkBranches c1 c2)
+             (mkBranches data)
              (tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype)))
       end }
     end
-- 
cgit v1.2.3


From 5c7163d2ee1412fa5af523fbcd275518fc61fbde Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 30 Apr 2017 12:14:38 +0200
Subject: Fix bug #5501: Universe polymorphism breaks proof involving auto.

A universe substitution was lacking as the normalized evar map was dropped.
---
 tactics/hints.ml | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'tactics')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index bcc068d3da..50b811edb1 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1238,18 +1238,15 @@ let prepare_hint check (poly,local) env init (sigma,c) =
   (* We re-abstract over uninstantiated evars and universes.
      It is actually a bit stupid to generalize over evars since the first
      thing make_resolves will do is to re-instantiate the products *)
-  let sigma, subst = Evd.nf_univ_variables sigma in
+  let sigma, _ = Evd.nf_univ_variables sigma in
   let c = Evarutil.nf_evar sigma c in
-  let c = EConstr.Unsafe.to_constr c in
-  let c = CVars.subst_univs_constr subst c in
-  let c = EConstr.of_constr c in
   let c = drop_extra_implicit_args sigma c in
   let vars = ref (collect_vars sigma c) in
   let subst = ref [] in
   let rec find_next_evar c = match EConstr.kind sigma c with
     | Evar (evk,args as ev) ->
       (* We skip the test whether args is the identity or not *)
-      let t = existential_type sigma ev in
+      let t = Evarutil.nf_evar sigma (existential_type sigma ev) in
       let t = List.fold_right (fun (e,id) c -> replace_term sigma e id c) !subst t in
       if not (closed0 sigma c) then
 	error "Hints with holes dependent on a bound variable not supported.";
-- 
cgit v1.2.3


From 2553e4bf5735a2bd127832e2d26609c6a8096fb7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 1 May 2017 17:24:29 +0200
Subject: Removing dead code in Autorewrite.

Since 260965d, an imperative code was semantically the identity because the
closure allocation was not performed at the right moment. Because of it
intricacy, I cannot really tell the original motivations of this piece of
code, although it looks like it was for there for pretty-printing of errors.
Anyway, both because the code was dubious and its effect not observed, it
cannot hurt to remove it.
---
 tactics/autorewrite.ml | 44 ++++++--------------------------------------
 1 file changed, 6 insertions(+), 38 deletions(-)

(limited to 'tactics')

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index e58ec5a31f..3c430cb174 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -127,45 +127,13 @@ let autorewrite ?(conds=Naive) tac_main lbas =
       (Proofview.tclUNIT()) lbas))
 
 let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
  (* let's check at once if id exists (to raise the appropriate error) *)
- let _ = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) idl in
- let general_rewrite_in id =
-  let id = ref id in
-  let to_be_cleared = ref false in
-   fun dir cstr tac gl ->
-    let last_hyp_id =
-     match Tacmach.pf_hyps gl with
-        d :: _ -> Context.Named.Declaration.get_id d
-      | _ -> (* even the hypothesis id is missing *)
-        raise (Logic.RefinerError (Logic.NoSuchHyp !id))
-    in
-    let gl' = Proofview.V82.of_tactic (general_rewrite_in dir AllOccurrences true ~tac:(tac, conds) false !id cstr false) gl in
-    let gls = gl'.Evd.it in
-    match gls with
-       g::_ ->
-        (match Environ.named_context_of_val (Goal.V82.hyps gl'.Evd.sigma g) with
-            d ::_ ->
-              let lastid = Context.Named.Declaration.get_id d in
-              if not (Id.equal last_hyp_id lastid) then
-               begin
-                let gl'' =
-                  if !to_be_cleared then
-                   tclTHEN (fun _ -> gl') (tclTRY (Proofview.V82.of_tactic (clear [!id]))) gl
-                  else gl' in
-                id := lastid ;
-                to_be_cleared := true ;
-                gl''
-               end
-              else
-               begin
-                to_be_cleared := false ;
-                gl'
-               end
-          | _ -> assert false) (* there must be at least an hypothesis *)
-     | _ -> assert false (* rewriting cannot complete a proof *)
- in
- let general_rewrite_in x y z w = Proofview.V82.tactic (general_rewrite_in x y (EConstr.of_constr z) w) in
+  let _ = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) idl in
+  let general_rewrite_in id dir cstr tac =
+    let cstr = EConstr.of_constr cstr in
+    general_rewrite_in dir AllOccurrences true ~tac:(tac, conds) false id cstr false
+  in
  Tacticals.New.tclMAP (fun id ->
   Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS
     (List.fold_left (fun tac bas ->
-- 
cgit v1.2.3


From d0252cac3167ef1e5cd26c1b9b40aea06d343413 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 1 May 2017 17:48:57 +0200
Subject: More consistent writing of de Bruijn.

---
 tactics/dnet.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/dnet.mli b/tactics/dnet.mli
index 9f29c60b60..565a916f8e 100644
--- a/tactics/dnet.mli
+++ b/tactics/dnet.mli
@@ -26,7 +26,7 @@
    distincts, or you'll get unexpected behaviours.
 
    Warning 2: This structure is perfect, i.e. the set of candidates
-   returned is equal to the set of solutions. Beware of DeBruijn
+   returned is equal to the set of solutions. Beware of de Bruijn
    shifts and sorts subtyping though (which makes the comparison not
    symmetric, see term_dnet.ml).
 
-- 
cgit v1.2.3


From cea40f37ab638031b9d5c6434ee5651a16ea1f3e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 1 May 2017 09:04:17 +0200
Subject: Fixing Set Rewriting Schemes bugs introduced in v8.5.

- Fixing a typo introduced in 31dbba5f.
- Adapting to computation of universe constraints in pretyping.
- Adding a regression test.
---
 tactics/eqschemes.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 1a45217a4a..e39159fb82 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -89,6 +89,11 @@ let get_coq_eq ctx =
   with Not_found ->
     error "eq not found."
 
+let univ_of_eq env eq =
+  match kind_of_term (Retyping.get_type_of env Evd.empty eq) with
+  | Prod (_,t,_) -> (match kind_of_term t with Sort (Type u) -> u | _ -> assert false)
+  | _ -> assert false
+
 (**********************************************************************)
 (* Check if an inductive type [ind] has the form                      *)
 (*                                                                    *)
@@ -744,7 +749,7 @@ let build_congr env (eq,refl,ctx) ind =
   let ty = get_type (lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity) in
   let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
-  if Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt) then
+  if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then
     error "Constructor must have no arguments";
   let b = List.nth constrargs (i + mib.mind_nparams - 1) in
   let varB = fresh env (Id.of_string "B") in
@@ -752,6 +757,7 @@ let build_congr env (eq,refl,ctx) ind =
   let varf = fresh env (Id.of_string "f") in
   let ci = make_case_info (Global.env()) ind RegularStyle in
   let uni, ctx = Universes.extend_context (Universes.new_global_univ ()) ctx in
+  let ctx = (fst ctx, Univ.enforce_leq uni (univ_of_eq env eq) (snd ctx)) in
   let c = 
   my_it_mkLambda_or_LetIn paramsctxt
      (mkNamedLambda varB (mkSort (Type uni))
-- 
cgit v1.2.3


From 874ff85e2d52b33010007bb3a1f1add9391b030f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 2 May 2017 16:33:59 +0200
Subject: Remove unused module definition after merging PR#592.

---
 tactics/hints.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index d57e4875c1..c5bacc5a20 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-module CVars = Vars
-
 open Pp
 open Util
 open CErrors
-- 
cgit v1.2.3


From 5548e5f6bc5446f7541cfc7d93b0b47e4b751e86 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 5 May 2017 15:39:17 +0200
Subject: Remove unused open.

---
 tactics/eqdecide.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 472cd8f22b..641929a77b 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -67,7 +67,6 @@ let choose_noteq eqonleft =
     left_with_bindings false Misctypes.NoBindings
 
 open Sigma.Notations
-open Context.Rel.Declaration
 
 (* A surgical generalize which selects the right occurrences by hand *)
 (* This prevents issues where c2 is also a subterm of c1 (see e.g. #5449) *)
-- 
cgit v1.2.3


From a76a71eda10b054b04de4ff56f0637a32077edd4 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 5 May 2017 18:09:30 +0200
Subject: Remove two unused opens.

---
 tactics/autorewrite.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 3c430cb174..2d54b61c72 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -9,8 +9,6 @@
 open Equality
 open Names
 open Pp
-open Tacticals
-open Tactics
 open Term
 open Termops
 open CErrors
-- 
cgit v1.2.3


From e0577588056110ea13a904aa1f01c86dbc931f02 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 11 May 2017 13:14:27 +0200
Subject: Remove an unused open introduced by the previous commit.

---
 tactics/tactics.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3842b432da..556df6e559 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5004,7 +5004,6 @@ let name_op_to_name name_op object_kind suffix =
       add_suffix name suffix, gk
 
 let tclABSTRACT ?(opaque=true) name_op tac =
-  let open Proof_global in
   let s, gk = if opaque
     then name_op_to_name name_op (Proof Theorem) "_subproof"
     else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in
-- 
cgit v1.2.3


From e3550a0acc39e235e01a727267b12a7c06f23b2c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 26 Aug 2016 14:46:33 +0200
Subject: Uniformity of style for selecting plural or not; spacing for comma.

---
 tactics/class_tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 2d6dffdd23..05eb0a9760 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1202,7 +1202,7 @@ module Search = struct
            Feedback.msg_debug
              (pr_depth info.search_depth ++ str": no match for " ++
                 Printer.pr_econstr_env (Goal.env gl) s concl ++
-                spc () ++ str ", " ++ int (List.length poss) ++
+                str ", " ++ int (List.length poss) ++
                 str" possibilities");
          match e with
          | (ReachedLimitEx,ie) -> Proofview.tclZERO ~info:ie ReachedLimitEx
-- 
cgit v1.2.3


From 94e8664074cfb987f8a63ca29c5436c861184b3a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 11 Sep 2016 11:55:08 +0200
Subject: Stopping injection not to work on discriminable atoms (see #4890).

---
 tactics/equality.ml  | 19 ++++++++++---------
 tactics/equality.mli |  3 +++
 2 files changed, 13 insertions(+), 9 deletions(-)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index cc7701ad5f..18a1f02011 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -736,7 +736,7 @@ let _ =
       optread  = (fun () -> !keep_proof_equalities_for_injection) ;
       optwrite = (fun b -> keep_proof_equalities_for_injection := b) }
 
-let find_positions env sigma t1 t2 =
+let find_positions env sigma ~no_discr t1 t2 =
   let project env sorts posn t1 t2 =
     let ty1 = get_type_of env sigma t1 in
     let s = get_sort_family_of env sigma ty1 in
@@ -767,7 +767,7 @@ let find_positions env sigma t1 t2 =
             List.flatten
 	      (List.map2_i (fun i -> findrec sorts' ((sp1,adjust i)::posn))
 		0 rargs1 rargs2)
-	  else if Sorts.List.mem InType sorts'
+	  else if Sorts.List.mem InType sorts' && not no_discr
           then (* see build_discriminator *)
 	    raise (DiscrFound (List.rev posn,sp1,sp2))
 	  else 
@@ -791,13 +791,14 @@ let find_positions env sigma t1 t2 =
     Inl (path,c1,c2)
 
 let discriminable env sigma t1 t2 =
-  match find_positions env sigma t1 t2 with
+  match find_positions env sigma ~no_discr:false t1 t2 with
     | Inl _ -> true
     | _ -> false
 
 let injectable env sigma t1 t2 =
-    match find_positions env sigma t1 t2 with
-    | Inl _ | Inr [] | Inr [([],_,_)] -> false
+    match find_positions env sigma ~no_discr:true t1 t2 with
+    | Inl _ -> assert false
+    | Inr [] | Inr [([],_,_)] -> false
     | Inr _ -> true
 
 
@@ -1032,7 +1033,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
   Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
-    match find_positions env sigma t1 t2 with
+    match find_positions env sigma ~no_discr:false t1 t2 with
     | Inr _ ->
 	tclZEROMSG (str"Not a discriminable equality.")
     | Inl (cpath, (_,dirn), _) ->
@@ -1414,9 +1415,9 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
 let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
   let env = eq_clause.env in
-  match find_positions env sigma t1 t2 with
+  match find_positions env sigma ~no_discr:true t1 t2 with
   | Inl _ ->
-     tclZEROMSG (strbrk"This equality is discriminable. You should use the discriminate tactic to solve the goal.")
+     assert false
   | Inr [] ->
      let suggestion =
          if !keep_proof_equalities_for_injection then
@@ -1483,7 +1484,7 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
   Proofview.Goal.enter { enter = begin fun gl ->
     let sigma =  clause.evd in
     let env = Proofview.Goal.env gl in
-      match find_positions env sigma t1 t2 with
+      match find_positions env sigma ~no_discr:false t1 t2 with
       | Inl (cpath, (_,dirn), _) ->
 	  discr_positions env sigma u clause cpath dirn
       | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
diff --git a/tactics/equality.mli b/tactics/equality.mli
index d979c580aa..b47be3bbc0 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -96,7 +96,10 @@ val cutRewriteInConcl : bool -> constr -> unit Proofview.tactic
 val rewriteInHyp : bool -> constr -> Id.t -> unit Proofview.tactic
 val rewriteInConcl : bool -> constr -> unit Proofview.tactic
 
+(* Tells if tactic "discriminate" is applicable *)
 val discriminable : env -> evar_map -> constr -> constr -> bool
+
+(* Tells if tactic "injection" is applicable *)
 val injectable : env -> evar_map -> constr -> constr -> bool
 
 (* Subst *)
-- 
cgit v1.2.3


From 741f3fab052b91eaec57f32b639ca722c3d8dc34 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 12 Mar 2017 13:18:42 +0100
Subject: A fix for #5390 (a useful error on used introduction names was
 masked).

With the "apply in" introduction pattern, and the backtrack possibly
done in "apply" over the components of conjunctions
(descend_in_conjunctions), the reasons for failing might have
different sources.

We give priority to the detection of used names over other
(unification) errors so that an error there is not masked in the
backtracking made by descend_in_conjunctions.

Of course, the question of what best unification error to give in the
presence of backtracking is still open.
---
 tactics/tactics.ml | 40 ++++++++++++++++++++++++++++++++++++----
 1 file changed, 36 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 556df6e559..15cef676e6 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2395,6 +2395,29 @@ let rec explicit_intro_names = function
      explicit_intro_names l
 | [] -> []
 
+let rec check_name_unicity env ok seen = function
+| (_, IntroForthcoming _) :: l -> check_name_unicity env ok seen l
+| (loc, IntroNaming (IntroIdentifier id)) :: l ->
+   (try
+      ignore (if List.mem_f Id.equal id ok then raise Not_found else lookup_named id env);
+      user_err ~loc (pr_id id ++ str" is already used.")
+   with Not_found ->
+     if List.mem_f Id.equal id seen then
+       user_err ~loc (pr_id id ++ str" is used twice.")
+     else
+       check_name_unicity env ok (id::seen) l)
+| (_, IntroAction (IntroOrAndPattern l)) :: l' ->
+    let ll = match l with IntroAndPattern l -> [l] | IntroOrPattern ll -> ll in
+    List.iter (fun l -> check_name_unicity env ok seen (l@l')) ll
+| (_, IntroAction (IntroInjection l)) :: l' ->
+    check_name_unicity env ok seen (l@l')
+| (_, IntroAction (IntroApplyOn (c,pat))) :: l' ->
+    check_name_unicity env ok seen (pat::l')
+| (_, (IntroNaming (IntroAnonymous | IntroFresh _)
+     | IntroAction (IntroWildcard | IntroRewrite _))) :: l ->
+     check_name_unicity env ok seen l
+| [] -> ()
+
 let wild_id = Id.of_string "_tmp"
 
 let rec list_mem_assoc_right id = function
@@ -2530,13 +2553,21 @@ and prepare_intros_loc loc with_evars dft destopt = function
   | IntroForthcoming _ -> user_err ~loc 
       (str "Introduction pattern for one hypothesis expected.")
 
+let intro_patterns_head_core with_evars b destopt bound pat =
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    check_name_unicity env [] [] pat;
+    intro_patterns_core with_evars b [] [] [] destopt
+      bound 0 (fun _ l -> clear_wildcards l) pat
+  end }
+
 let intro_patterns_bound_to with_evars n destopt =
-  intro_patterns_core with_evars true [] [] [] destopt
-    (Some (true,n)) 0 (fun _ l -> clear_wildcards l)
+  intro_patterns_head_core with_evars true destopt
+    (Some (true,n))
 
 let intro_patterns_to with_evars destopt =
-  intro_patterns_core with_evars (use_bracketing_last_or_and_intro_pattern ())
-    [] [] [] destopt None 0 (fun _ l -> clear_wildcards l)
+  intro_patterns_head_core with_evars (use_bracketing_last_or_and_intro_pattern ())
+    destopt None
 
 let intro_pattern_to with_evars destopt pat =
   intro_patterns_to with_evars destopt [dloc,pat]
@@ -4191,6 +4222,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_
       let f (_,is_not_let,_,_) = is_not_let in
       Array.map (fun (_,l) -> List.map f l) indsign in
     let names = compute_induction_names branchletsigns names in
+    Array.iter (check_name_unicity env toclear []) names;
     let tac =
     (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn)
       (Tacticals.New.tclTHENLIST [
-- 
cgit v1.2.3