From 6ebd2316e5acf10e0d505804fdd7001edc5575fa Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 5 May 2015 11:54:49 +0200
Subject: Making the strategy type in Rewrite opaque.

---
 tactics/rewrite.mli | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli
index cae00f5a86..40a18ac458 100644
--- a/tactics/rewrite.mli
+++ b/tactics/rewrite.mli
@@ -55,10 +55,7 @@ type rewrite_result =
 | Identity
 | Success of rewrite_result_info
 
-type 'a pure_strategy = 'a -> Environ.env -> Id.t list -> constr -> types ->
-  (bool (* prop *) * constr option) -> evars -> 'a * rewrite_result
-
-type strategy = unit pure_strategy
+type strategy
 
 val strategy_of_ast : (glob_constr_and_expr, raw_red_expr) strategy_ast -> strategy
 
-- 
cgit v1.2.3


From e4ca462b7d51f25b258263345835025c1c4325bd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 5 May 2015 12:28:42 +0200
Subject: Removing dead code in Rewrite.

The hypinfo cache was actually always set to None, so that there was no need
to try to preserve it if it was set to an actual value.
---
 tactics/rewrite.ml | 64 ++++++++++++++++++++----------------------------------
 1 file changed, 23 insertions(+), 41 deletions(-)

(limited to 'tactics')

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 60ce0e0dc3..1be394aa4a 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -452,7 +452,6 @@ let convertible env evd x y =
   Reductionops.is_conv_leq env evd x y
 
 type hypinfo = {
-  env : env;
   prf : constr;
   car : constr;
   rel : constr;
@@ -498,7 +497,7 @@ let decompose_applied_relation env sigma (c,l) =
       let sort = sort_of_rel env sigma equiv in
       let args = Array.map_of_list (fun h -> h.Clenv.hole_evar) holes in
       let value = mkApp (c, args) in
-        Some (sigma, { env=env; prf=value;
+        Some (sigma, { prf=value;
                 car=ty1; rel = equiv; sort = Sorts.is_prop sort;
                 c1=c1; c2=c2; holes })
   in
@@ -510,10 +509,6 @@ let decompose_applied_relation env sigma (c,l) =
 	| Some c -> c
 	| None -> error "Cannot find an homogeneous relation to rewrite."
 
-let decompose_applied_relation_expr env sigma (is, (c,l)) =
-  let sigma, cbl = Tacinterp.interp_open_constr_with_bindings is env sigma (c,l) in
-  decompose_applied_relation env sigma cbl
-
 let rewrite_db = "rewrite"
 
 let conv_transparent_state = (Id.Pred.empty, Cpred.full)
@@ -588,24 +583,12 @@ let general_rewrite_unif_flags () =
     Unification.resolve_evars = true
   }
 
-let refresh_hypinfo env sigma hypinfo c =
-  let sigma, hypinfo = match hypinfo with
-  | None ->
-    decompose_applied_relation_expr env sigma c
-  | Some hypinfo ->
-    if hypinfo.env != env then
-      (* If the lemma actually generates existential variables, we cannot 
-          use it here as it will polute the evar map with existential variables
-          that might not ever get instantiated (e.g. if we rewrite under a
-          binder and need to refresh [c] again) *)
-      (* TODO: remove bindings in sigma corresponding to c *)
-      decompose_applied_relation_expr env sigma c
-    else sigma, hypinfo
-  in
+let refresh_hypinfo env sigma (is, cb) =
+  let sigma, cbl = Tacinterp.interp_open_constr_with_bindings is env sigma cb in
+  let sigma, hypinfo = decompose_applied_relation env sigma cbl in
   let { c1; c2; car; rel; prf; sort; holes } = hypinfo in
   sigma, (car, rel, prf, c1, c2, holes, sort)
 
-
 (** FIXME: write this in the new monad interface *)
 let solve_remaining_by env sigma holes by =
   match by with
@@ -719,7 +702,7 @@ let unify_abs (car, rel, prf, c1, c2) l2r sort env (sigma, cstrs) t =
     let rew_prf = RewPrf (rel, prf) in
     let rew = { rew_car = car; rew_from = c1; rew_to = c2; rew_prf; rew_evars; } in
     let rew = if l2r then rew else symmetry env sort rew in
-    Some ((), rew)
+    Some rew
   with 
   | e when Class_tactics.catchable e -> None
   | Reduction.NotConvertible -> None
@@ -829,27 +812,27 @@ let coerce env avoid cstr res =
   let rel, prf = get_rew_prf res in
     apply_constraint env avoid res.rew_car rel prf cstr res
 
-let apply_rule unify loccs : ('a * int) pure_strategy =
+let apply_rule unify loccs : int pure_strategy =
   let (nowhere_except_in,occs) = convert_occs loccs in
   let is_occ occ =
     if nowhere_except_in 
     then List.mem occ occs 
     else not (List.mem occ occs) 
   in
-    fun (hypinfo, occ) env avoid t ty cstr evars ->
-      let unif = if isEvar t then None else unify hypinfo env evars t in
+    fun occ env avoid t ty cstr evars ->
+      let unif = if isEvar t then None else unify env evars t in
 	match unif with
-	| None -> ((hypinfo, occ), Fail)
-        | Some (hypinfo', rew) ->
+	| None -> (occ, Fail)
+        | Some rew ->
 	  let occ = succ occ in
-	    if not (is_occ occ) then ((hypinfo, occ), Fail)
-	    else if eq_constr t rew.rew_to then ((hypinfo, occ), Identity)
+	    if not (is_occ occ) then (occ, Fail)
+	    else if eq_constr t rew.rew_to then (occ, Identity)
 	    else
 	      let res = { rew with rew_car = ty } in
               let rel, prf = get_rew_prf res in
 	      let res = Success (apply_constraint env avoid rew.rew_car rel prf cstr res) in
-		((hypinfo', occ), res)
-		  
+              (occ, res)
+
 let apply_lemma l2r flags oc by loccs : strategy =
   fun () env avoid t ty cstr (sigma, cstrs) ->
     let sigma, c = oc sigma in
@@ -857,13 +840,13 @@ let apply_lemma l2r flags oc by loccs : strategy =
     let { c1; c2; car; rel; prf; sort; holes } = hypinfo in
     let rew = (car, rel, prf, c1, c2, holes, sort) in
     let evars = (sigma, cstrs) in
-    let unify () env evars t =
+    let unify env evars t =
       let rew = unify_eqn rew l2r flags env evars by t in
       match rew with
       | None -> None
-      | Some rew -> Some ((), rew)
+      | Some rew -> Some rew
     in
-    let _, res = apply_rule unify loccs ((), 0) env avoid t ty cstr evars in
+    let _, res = apply_rule unify loccs 0 env avoid t ty cstr evars in
     (), res
 
 let e_app_poly env evars f args =
@@ -1379,11 +1362,10 @@ end
 
 let rewrite_with l2r flags c occs : strategy =
   fun () env avoid t ty cstr (sigma, cstrs) ->
-    let hypinfo = None in
-    let unify hypinfo env evars t =
+    let unify env evars t =
       let (sigma, cstrs) = evars in
       let ans =
-        try Some (refresh_hypinfo env sigma hypinfo c)
+        try Some (refresh_hypinfo env sigma c)
         with e when Class_tactics.catchable e -> None
       in
       match ans with
@@ -1392,14 +1374,14 @@ let rewrite_with l2r flags c occs : strategy =
         let rew = unify_eqn rew l2r flags env (sigma, cstrs) None t in
         match rew with
         | None -> None
-        | Some rew -> Some (None, rew) (** reset the hypinfo cache *)
+        | Some rew -> Some rew
     in
     let app = apply_rule unify occs in
     let strat = 
       Strategies.fix (fun aux -> 
 	Strategies.choice app (subterm true default_flags aux))
     in
-    let _, res = strat (hypinfo, 0) env avoid t ty cstr (sigma, cstrs) in
+    let _, res = strat 0 env avoid t ty cstr (sigma, cstrs) in
       ((), res)
 
 let apply_strategy (s : strategy) env avoid concl (prop, cstr) evars =
@@ -1967,12 +1949,12 @@ let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
 (** Setoid rewriting when called with "rewrite" *)
 let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
   let abs, evd, res, sort = get_hyp gl (c,l) cl l2r in
-  let unify () env evars t = unify_abs res l2r sort env evars t in
+  let unify env evars t = unify_abs res l2r sort env evars t in
   let app = apply_rule unify occs in
   let recstrat aux = Strategies.choice app (subterm true general_rewrite_flags aux) in
   let substrat = Strategies.fix recstrat in
   let strat () env avoid t ty cstr evars =
-    let _, res = substrat ((), 0) env avoid t ty cstr evars in
+    let _, res = substrat 0 env avoid t ty cstr evars in
     (), res
   in
   let origsigma = project gl in
-- 
cgit v1.2.3


From 5a0d3395cd972393eaa7859f47a738cc99ea55c6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 6 May 2015 12:35:42 +0200
Subject: Fixing "subst" to respect v8.4 most-ancient to most-recent hyps order
 after patch for #4214 on subst needed to be repeated (see 857e82b2ca0d1).

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

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index f2860a2300..c5b87761d8 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1681,7 +1681,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
       with Constr_matching.PatternMatchingFailure -> None
     in
     let hyps = Proofview.Goal.hyps gl in
-    List.map_filter test hyps
+    List.rev (List.map_filter test hyps)
   in
 
   (* Second step: treat equations *)
-- 
cgit v1.2.3


From 32a9a4e3656e581af41c26f48f63ed1daec331d8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 6 May 2015 18:54:18 +0200
Subject: Fixing treatment of recursive equations damaged by 857e82b2ca0d1.
 Improving treatment of recursive equations compared to 8.4 (see test-suite).
 Experimenting not to unfold local defs ever in subst. (+ Slight
 simplification in checking reflexive equalities only once).

---
 tactics/equality.ml | 18 +++++++++++-------
 1 file changed, 11 insertions(+), 7 deletions(-)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index c5b87761d8..591fbabaef 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1667,17 +1667,18 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
   (* First step: find hypotheses to treat in linear time *)
   let find_equations gl =
     let gl = Proofview.Goal.assume gl in
+    let env = Proofview.Goal.env gl in
     let find_eq_data_decompose = find_eq_data_decompose gl in
     let test (hyp,_,c) =
       try
         let lbeq,u,(_,x,y) = find_eq_data_decompose c in
         let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
         if flags.only_leibniz then restrict_to_eq_and_identity eq;
-        (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
-        if Term.eq_constr x y then None else
         match kind_of_term x, kind_of_term y with
-        | Var _, _ | _, Var _ -> Some hyp
-        | _ -> None
+        | Var z, _ | _, Var z when not (is_evaluable env (EvalVarRef z))  ->
+            Some hyp
+        | _ ->
+            None
       with Constr_matching.PatternMatchingFailure -> None
     in
     let hyps = Proofview.Goal.hyps gl in
@@ -1694,9 +1695,12 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
     (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
     if Term.eq_constr x y then Proofview.tclUNIT () else
       match kind_of_term x, kind_of_term y with
-      | Var x, _ -> subst_one flags.rewrite_dependent_proof x (hyp,y,true)
-      | _, Var y -> subst_one flags.rewrite_dependent_proof y (hyp,x,false)
-      | _ -> Proofview.tclUNIT ()
+      | Var x', _ when not (occur_term x y) ->
+          subst_one flags.rewrite_dependent_proof x' (hyp,y,true)
+      | _, Var y' when not (occur_term y x) ->
+          subst_one flags.rewrite_dependent_proof y' (hyp,x,false)
+      | _ ->
+          Proofview.tclUNIT ()
     end
   in
   Proofview.Goal.nf_enter begin fun gl ->
-- 
cgit v1.2.3


From 5cbc018fe934750bdf1043da68f99911be4ee6f6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 5 May 2015 19:25:24 +0200
Subject: Adding a flag "Set Regular Subst Tactic" off by default in v8.5 for
 preserving compatibility of subst after #4214 being solved.

---
 tactics/equality.ml | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 591fbabaef..593b7e9ea0 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1662,8 +1662,21 @@ let default_subst_tactic_flags () =
   else
     { only_leibniz = true; rewrite_dependent_proof = false }
 
+let regular_subst_tactic = ref false
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "more regular behavior of tactic subst";
+      optkey   = ["Regular";"Subst";"Tactic"];
+      optread  = (fun () -> !regular_subst_tactic);
+      optwrite = (:=) regular_subst_tactic }
+
 let subst_all ?(flags=default_subst_tactic_flags ()) () =
 
+  if !regular_subst_tactic then
+
   (* First step: find hypotheses to treat in linear time *)
   let find_equations gl =
     let gl = Proofview.Goal.assume gl in
@@ -1708,6 +1721,30 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
     tclMAP process ids
   end
 
+  else
+
+(* Old implementation, not able to manage configurations like a=b, a=t,
+   or situations like "a = S b, b = S a", or also accidentally unfolding
+   let-ins *)
+  Proofview.Goal.nf_enter begin fun gl ->
+  let find_eq_data_decompose = find_eq_data_decompose gl in
+  let test (_,c) =
+    try
+      let lbeq,u,(_,x,y) = find_eq_data_decompose c in
+      let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
+      if flags.only_leibniz then restrict_to_eq_and_identity eq;
+      (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
+      if Term.eq_constr x y then failwith "caught";
+      match kind_of_term x with Var x -> x | _ ->
+      match kind_of_term y with Var y -> y | _ -> failwith "caught"
+    with Constr_matching.PatternMatchingFailure -> failwith "caught" in
+  let test p = try Some (test p) with Failure _ -> None in
+  let hyps = pf_hyps_types gl in
+  let ids = List.map_filter test hyps in
+  let ids = List.uniquize ids in
+  subst_gen flags.rewrite_dependent_proof ids
+  end
+
 (* Rewrite the first assumption for which a condition holds
    and gives the direction of the rewrite *)
 
-- 
cgit v1.2.3


From 9a883e3740e21c93c8ea7f51b0cf0c4a76675773 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 11 May 2015 08:34:50 +0200
Subject: Rationalizing a bit the interface of Hints.

---
 tactics/auto.ml          |  2 +-
 tactics/auto.mli         |  2 +-
 tactics/class_tactics.ml |  8 ++++----
 tactics/eauto.ml4        |  4 ++--
 tactics/hints.ml         | 28 ++++++++++++++--------------
 tactics/hints.mli        | 28 ++++++++++++++--------------
 6 files changed, 36 insertions(+), 36 deletions(-)

(limited to 'tactics')

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 7da8415714..72ba9e0bd9 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -377,7 +377,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly}))
     | Extern tacast -> 
       conclPattern concl p tacast
   in
-  tclLOG dbg (fun () -> pr_autotactic t) (run_auto_tactic t tactic)
+  tclLOG dbg (fun () -> pr_hint t) (run_hint t tactic)
 
 and trivial_resolve dbg mod_delta db_list local_db cl =
   try
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 0cc8a0b1b9..8dacc13629 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -19,7 +19,7 @@ val extern_interp :
 
 (** Auto and related automation tactics *)
 
-val priority : ('a * pri_auto_tactic) list -> ('a * pri_auto_tactic) list
+val priority : ('a * full_hint) list -> ('a * full_hint) list
 
 val default_search_depth : int ref
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index e11458c049..6ea25269cf 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -231,13 +231,13 @@ and e_my_find_search db_list local_db hdc complete sigma concl =
       | Unfold_nth c -> Proofview.V82.tactic (tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c]))
       | Extern tacast -> conclPattern concl p tacast
       in
-      let tac = Proofview.V82.of_tactic (run_auto_tactic t tac) in
+      let tac = Proofview.V82.of_tactic (run_hint t tac) in
       let tac = if complete then tclCOMPLETE tac else tac in
-	match repr_auto_tactic t with
-	| Extern _ -> (tac,b,true, name, lazy (pr_autotactic t))
+	match repr_hint t with
+	| Extern _ -> (tac,b,true, name, lazy (pr_hint t))
 	| _ ->
 (* 	  let tac gl = with_pattern (pf_env gl) (project gl) flags p concl tac gl in *)
-	    (tac,b,false, name, lazy (pr_autotactic t))
+	    (tac,b,false, name, lazy (pr_hint t))
   in List.map tac_of_hint hintl
 
 and e_trivial_resolve db_list local_db sigma concl =
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index d738677e50..50925ecde6 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -172,8 +172,8 @@ and e_my_find_search db_list local_db hdc concl =
         | Unfold_nth c -> Proofview.V82.tactic (reduce (Unfold [AllOccurrences,c]) onConcl)
         | Extern tacast -> conclPattern concl p tacast
        in
-       let tac = Proofview.V82.of_tactic (run_auto_tactic t tac) in
-       (tac, lazy (pr_autotactic t)))
+       let tac = Proofview.V82.of_tactic (run_hint t tac) in
+       (tac, lazy (pr_hint t)))
   in
   List.map tac_of_hint hintl
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index f83aa56017..b8e4dd9fa4 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -68,7 +68,7 @@ let decompose_app_bound t =
 (*           The Type of Constructions Autotactic Hints                 *)
 (************************************************************************)
 
-type 'a auto_tactic_ast =
+type 'a hint_ast =
   | Res_pf     of 'a (* Hint Apply *)
   | ERes_pf    of 'a (* Hint EApply *)
   | Give_exact of 'a
@@ -92,9 +92,9 @@ type hint_term =
   | IsGlobRef of global_reference
   | IsConstr of constr * Univ.universe_context_set
 
-type 'a auto_tactic = 'a auto_tactic_ast
+type hint = (constr * clausenv) hint_ast
 
-type 'a gen_auto_tactic = {
+type 'a with_metadata = {
   pri  : int;            (* A number lower is higher priority *)
   poly  : polymorphic;    (** Is the hint polymorpic and hence should be refreshed at each application *)
   pat  : constr_pattern option; (* A pattern for the concl of the Goal *)
@@ -102,13 +102,13 @@ type 'a gen_auto_tactic = {
   code : 'a     (* the tactic to apply when the concl matches pat *)
 }
 
-type pri_auto_tactic = (constr * clausenv) auto_tactic gen_auto_tactic
+type full_hint = hint with_metadata
 
 type hint_entry = global_reference option * 
-  (constr * types * Univ.universe_context_set) auto_tactic_ast gen_auto_tactic
+  (constr * types * Univ.universe_context_set) hint_ast with_metadata
 
-let run_auto_tactic tac k = k tac
-let repr_auto_tactic tac = tac
+let run_hint tac k = k tac
+let repr_hint h = h
 
 let eq_hints_path_atom p1 p2 = match p1, p2 with
 | PathHints gr1, PathHints gr2 -> List.equal eq_gr gr1 gr2
@@ -125,7 +125,7 @@ let eq_auto_tactic t1 t2 = match t1, t2 with
 | (Res_pf _ | ERes_pf _ | Give_exact _ | Res_pf_THEN_trivial_fail _
   | Unfold_nth _ | Extern _), _ -> false
 
-let eq_gen_auto_tactic t1 t2 =
+let eq_hint_metadata t1 t2 =
   Int.equal t1.pri t2.pri &&
   Option.equal constr_pattern_eq t1.pat t2.pat &&
   eq_hints_path_atom t1.name t2.name &&
@@ -153,7 +153,7 @@ let pri_order t1 t2 = pri_order_int t1 t2 <= 0
      - un discrimination net borné (Btermdn.t) constitué de tous les
        patterns de la seconde liste de tactiques *)
 
-type stored_data = int * pri_auto_tactic
+type stored_data = int * full_hint
     (* First component is the index of insertion in the table, to keep most recent first semantics. *)
 
 module Bounded_net = Btermdn.Make(struct
@@ -481,7 +481,7 @@ module Hint_db = struct
       match k with
       | None ->
           (** ppedrot: this equality here is dubious. Maybe we can remove it? *)
-          let is_present (_, (_, v')) = eq_gen_auto_tactic v v' in
+          let is_present (_, (_, v')) = eq_hint_metadata v v' in
 	  if not (List.exists is_present db.hintdb_nopat) then
 	    (** FIXME *)
 	    { db with hintdb_nopat = (gr,idv) :: db.hintdb_nopat }
@@ -1146,7 +1146,7 @@ let make_db_list dbnames =
 (*                    Functions for printing the hints                    *)
 (**************************************************************************)
 
-let pr_autotactic =
+let pr_hint =
   function
   | Res_pf (c,clenv) -> (str"apply " ++ pr_constr c)
   | ERes_pf (c,clenv) -> (str"eapply " ++ pr_constr c)
@@ -1163,11 +1163,11 @@ let pr_autotactic =
       in
       (str "(*external*) " ++ Pptactic.pr_glob_tactic env tac)
 
-let pr_hint (id, v) =
-  (pr_autotactic v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ())
+let pr_id_hint (id, v) =
+  (pr_hint v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ())
 
 let pr_hint_list hintlist =
-  (str "  " ++ hov 0 (prlist pr_hint hintlist) ++ fnl ())
+  (str "  " ++ hov 0 (prlist pr_id_hint hintlist) ++ fnl ())
 
 let pr_hints_db (name,db,hintlist) =
   (str "In the database " ++ str name ++ str ":" ++
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 958cca1c3b..687bc78c76 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -28,7 +28,7 @@ val decompose_app_bound : constr -> global_reference * constr array
 
 (** Pre-created hint databases *)
 
-type 'a auto_tactic_ast =
+type 'a hint_ast =
   | Res_pf     of 'a (* Hint Apply *)
   | ERes_pf    of 'a (* Hint EApply *)
   | Give_exact of 'a
@@ -36,13 +36,13 @@ type 'a auto_tactic_ast =
   | Unfold_nth of evaluable_global_reference       (* Hint Unfold *)
   | Extern     of Tacexpr.glob_tactic_expr       (* Hint Extern *)
 
-type 'a auto_tactic
+type hint
 
 type hints_path_atom = 
   | PathHints of global_reference list
   | PathAny
 
-type 'a gen_auto_tactic = private {
+type 'a with_metadata = private {
   pri   : int;            (** A number between 0 and 4, 4 = lower priority *)
   poly  : polymorphic;    (** Is the hint polymorpic and hence should be refreshed at each application *)
   pat   : constr_pattern option; (** A pattern for the concl of the Goal *)
@@ -50,7 +50,7 @@ type 'a gen_auto_tactic = private {
   code  : 'a; (** the tactic to apply when the concl matches pat *)
 }
 
-type pri_auto_tactic = (constr * clausenv) auto_tactic gen_auto_tactic
+type full_hint = hint with_metadata
 
 type search_entry
 
@@ -76,28 +76,28 @@ module Hint_db :
     type t
     val empty : transparent_state -> bool -> t
     val find : global_reference -> t -> search_entry
-    val map_none : t -> pri_auto_tactic list
+    val map_none : t -> full_hint list
 
     (** All hints associated to the reference *)
-    val map_all : global_reference -> t -> pri_auto_tactic list
+    val map_all : global_reference -> t -> full_hint list
 
     (** All hints associated to the reference, respecting modes if evars appear in the 
 	arguments, _not_ using the discrimination net. *)
-    val map_existential : (global_reference * constr array) -> constr -> t -> pri_auto_tactic list
+    val map_existential : (global_reference * constr array) -> constr -> t -> full_hint list
 
     (** All hints associated to the reference, respecting modes if evars appear in the 
 	arguments and using the discrimination net. *)
-    val map_eauto : (global_reference * constr array) -> constr -> t -> pri_auto_tactic list
+    val map_eauto : (global_reference * constr array) -> constr -> t -> full_hint list
 
     (** All hints associated to the reference, respecting modes if evars appear in the 
 	arguments. *)
-    val map_auto : (global_reference * constr array) -> constr -> t -> pri_auto_tactic list
+    val map_auto : (global_reference * constr array) -> constr -> t -> full_hint list
 
     val add_one : hint_entry -> t -> t
     val add_list : (hint_entry) list -> t -> t
     val remove_one : global_reference -> t -> t
     val remove_list : global_reference list -> t -> t
-    val iter : (global_reference option -> bool array list -> pri_auto_tactic list -> unit) -> t -> unit
+    val iter : (global_reference option -> bool array list -> full_hint list -> unit) -> t -> unit
 
     val use_dn : t -> bool
     val transparent_state : t -> transparent_state
@@ -197,12 +197,12 @@ val make_extern :
   int -> constr_pattern option -> Tacexpr.glob_tactic_expr
       -> hint_entry
 
-val run_auto_tactic : 'a auto_tactic ->
-  ('a auto_tactic_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
+val run_hint : hint ->
+  ((constr * clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
 
 (** This function is for backward compatibility only, not to use in newly
     written code. *)
-val repr_auto_tactic : 'a auto_tactic -> 'a auto_tactic_ast
+val repr_hint : hint -> (constr * clausenv) hint_ast
 
 val extern_intern_tac :
   (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t
@@ -227,7 +227,7 @@ val pr_applicable_hint : unit -> std_ppcmds
 val pr_hint_ref : global_reference -> std_ppcmds
 val pr_hint_db_by_name : hint_db_name -> std_ppcmds
 val pr_hint_db : Hint_db.t -> std_ppcmds
-val pr_autotactic : (constr * 'a) auto_tactic -> Pp.std_ppcmds
+val pr_hint : hint -> Pp.std_ppcmds
 
 (** Hook for changing the initialization of auto *)
 
-- 
cgit v1.2.3


From 138bd9756a0fc80647427b2894ba4485f3e6961b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 11 May 2015 11:06:32 +0200
Subject: Fixing bug #4232.

We beta-iota normalize the type of the rewriting predicate to ensure that the
non-dependency in the arrow argument is meaningful. Otherwise, terms of the
form "forall x : A, (fun _ : A => P) x" generated by the retyping would confuse
the non-dependency heuristic.
---
 tactics/rewrite.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'tactics')

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 1be394aa4a..d487317736 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -226,6 +226,7 @@ end) = struct
       let t = Reductionops.whd_betadeltaiota env (goalevars evars) ty in
 	match kind_of_term t, l with
 	| Prod (na, ty, b), obj :: cstrs ->
+          let b = Reductionops.nf_betaiota (goalevars evars) b in
 	  if noccurn 1 b (* non-dependent product *) then
 	    let ty = Reductionops.nf_betaiota (goalevars evars) ty in
 	    let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in
-- 
cgit v1.2.3


From 2a2d418971a019202cdb78fabc7658a543f0886d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 11 May 2015 18:18:07 +0200
Subject: Adding a test to check whether two tactic notations conflict.

---
 tactics/tacenv.ml  | 2 ++
 tactics/tacenv.mli | 3 +++
 2 files changed, 5 insertions(+)

(limited to 'tactics')

diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index ffff44d5bc..08e8bc0112 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -26,6 +26,8 @@ let interp_alias key =
   try KNmap.find key !alias_map
   with Not_found -> Errors.anomaly (str "Unknown tactic alias: " ++ KerName.print key)
 
+let check_alias key = KNmap.mem key !alias_map
+
 (** ML tactic extensions (TacML) *)
 
 type ml_tactic =
diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli
index 29677fd4ca..9410ccb389 100644
--- a/tactics/tacenv.mli
+++ b/tactics/tacenv.mli
@@ -23,6 +23,9 @@ val register_alias : alias -> glob_tactic_expr -> unit
 val interp_alias : alias -> glob_tactic_expr
 (** Recover the the body of an alias. Raises an anomaly if it does not exist. *)
 
+val check_alias : alias -> bool
+(** Returns [true] if an alias is defined, false otherwise. *)
+
 (** {5 Coq tactic definitions} *)
 
 val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit
-- 
cgit v1.2.3


From 19752ec7e7ec2a89e01c9c65b1cc472cca04e424 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 15 Apr 2015 14:17:31 +0200
Subject: Adding unique identifiers to hints.

---
 tactics/hints.ml | 101 ++++++++++++++++++++++++++++++-------------------------
 1 file changed, 55 insertions(+), 46 deletions(-)

(limited to 'tactics')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index b8e4dd9fa4..5a5be1cbc5 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -92,23 +92,43 @@ type hint_term =
   | IsGlobRef of global_reference
   | IsConstr of constr * Univ.universe_context_set
 
-type hint = (constr * clausenv) hint_ast
+type 'a with_uid = {
+  obj : 'a;
+  uid : KerName.t;
+}
+
+type hint = (constr * clausenv) hint_ast with_uid
 
 type 'a with_metadata = {
   pri  : int;            (* A number lower is higher priority *)
   poly  : polymorphic;    (** Is the hint polymorpic and hence should be refreshed at each application *)
   pat  : constr_pattern option; (* A pattern for the concl of the Goal *)
   name  : hints_path_atom; (* A potential name to refer to the hint *) 
-  code : 'a     (* the tactic to apply when the concl matches pat *)
+  code : 'a;     (* the tactic to apply when the concl matches pat *)
 }
 
 type full_hint = hint with_metadata
 
 type hint_entry = global_reference option * 
-  (constr * types * Univ.universe_context_set) hint_ast with_metadata
-
-let run_hint tac k = k tac
-let repr_hint h = h
+  (constr * types * Univ.universe_context_set) hint_ast with_uid with_metadata
+
+let run_hint tac k = k tac.obj
+let repr_hint h = h.obj
+
+let fresh_key =
+  let id = Summary.ref ~name:"HINT-COUNTER" 0 in
+  fun () ->
+    let cur = incr id; !id in
+    let lbl = Id.of_string ("_" ^ string_of_int cur) in
+    let kn = Lib.make_kn lbl in
+    let (mp, dir, _) = KerName.repr kn in
+    (** We embed the full path of the kernel name in the label so that the
+        identifier should be unique. This ensures that including two modules
+        together won't confuse the corresponding labels. *)
+    let lbl = Id.of_string_soft (Printf.sprintf "%s#%s#%i"
+      (ModPath.to_string mp) (DirPath.to_string dir) cur)
+    in
+    KerName.make mp dir (Label.of_id lbl)
 
 let eq_hints_path_atom p1 p2 = match p1, p2 with
 | PathHints gr1, PathHints gr2 -> List.equal eq_gr gr1 gr2
@@ -175,21 +195,7 @@ let empty_se = {
   sentry_mode = [];
 }
 
-let eq_pri_auto_tactic (_, x) (_, y) =
-  if Int.equal x.pri y.pri && Option.equal constr_pattern_eq x.pat y.pat then
-    match x.code,y.code with
-      | Res_pf (cstr,_),Res_pf (cstr1,_) -> 
-	  Term.eq_constr cstr cstr1
-      | ERes_pf (cstr,_),ERes_pf (cstr1,_) -> 
-	  Term.eq_constr cstr cstr1
-      | Give_exact (cstr,_),Give_exact (cstr1,_)  -> 
-	  Term.eq_constr cstr cstr1
-      | Res_pf_THEN_trivial_fail (cstr,_)
-	  ,Res_pf_THEN_trivial_fail (cstr1,_) -> 
-	  Term.eq_constr cstr cstr1
-      | _,_ -> false
-  else
-    false
+let eq_pri_auto_tactic (_, x) (_, y) = KerName.equal x.code.uid y.code.uid
 
 let add_tac pat t st se =
   match pat with
@@ -248,7 +254,7 @@ let instantiate_hint p =
 	  { cl.templval with rebus = strip_params env cl.templval.rebus };
 	env = empty_env}
   in
-  let code = match p.code with
+  let code = match p.code.obj with
     | Res_pf (c, cty, ctx) -> Res_pf (c, mk_clenv c cty ctx)
     | ERes_pf (c, cty, ctx) -> ERes_pf (c, mk_clenv c cty ctx)
     | Res_pf_THEN_trivial_fail (c, cty, ctx) ->
@@ -256,7 +262,8 @@ let instantiate_hint p =
     | Give_exact (c, cty, ctx) -> Give_exact (c, mk_clenv c cty ctx)
     | Unfold_nth e -> Unfold_nth e
     | Extern t -> Extern t
-  in { pri = p.pri; poly = p.poly; name = p.name; pat = p.pat; code = code }
+  in
+  { p with code = { p.code with obj = code } }
 
 let hints_path_atom_eq h1 h2 = match h1, h2 with
 | PathHints l1, PathHints l2 -> List.equal eq_gr l1 l2
@@ -473,15 +480,14 @@ module Hint_db = struct
     let idv = id, v in
     let k = match gr with
       | Some gr -> if db.use_dn && is_transparent_gr db.hintdb_state gr &&
-	  is_unfold v.code then None else Some gr
+	  is_unfold v.code.obj then None else Some gr
       | None -> None
     in
     let dnst = if db.use_dn then Some db.hintdb_state else None in
-    let pat = if not db.use_dn && is_exact v.code then None else v.pat in
+    let pat = if not db.use_dn && is_exact v.code.obj then None else v.pat in
       match k with
       | None ->
-          (** ppedrot: this equality here is dubious. Maybe we can remove it? *)
-          let is_present (_, (_, v')) = eq_hint_metadata v v' in
+          let is_present (_, (_, v')) = KerName.equal v.code.uid v'.code.uid in
 	  if not (List.exists is_present db.hintdb_nopat) then
 	    (** FIXME *)
 	    { db with hintdb_nopat = (gr,idv) :: db.hintdb_nopat }
@@ -500,7 +506,7 @@ module Hint_db = struct
   let add_one (k, v) db =
     let v = instantiate_hint v in
     let st',db,rebuild =
-      match v.code with
+      match v.code.obj with
       | Unfold_nth egr ->
 	  let addunf (ids,csts) (ids',csts') =
 	    match egr with
@@ -632,6 +638,8 @@ let try_head_pattern c =
   try head_pattern_bound c
   with BoundPattern -> error "Bound head variable."
 
+let with_uid c = { obj = c; uid = fresh_key () }
+
 let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
   let cty = strip_outer_cast cty in
     match kind_of_term cty with
@@ -647,7 +655,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
 	    poly = poly;
 	    pat = Some pat;
 	    name = name;
-	    code = Give_exact (c, cty, ctx) })
+	    code = with_uid (Give_exact (c, cty, ctx)); })
 
 let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, cty, ctx) =
   let cty = if hnf then hnf_constr env sigma cty else cty in
@@ -667,7 +675,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
 	    poly = poly;
             pat = Some pat;
 	    name = name;
-            code = Res_pf(c,cty,ctx) })
+            code = with_uid (Res_pf(c,cty,ctx)); })
 	else begin
 	  if not eapply then failwith "make_apply_entry";
           if verbose then
@@ -678,7 +686,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
 	     poly = poly;
              pat = Some pat;
 	     name = name;
-             code = ERes_pf(c,cty,ctx) })
+             code = with_uid (ERes_pf(c,cty,ctx)); })
         end
     | _ -> failwith "make_apply_entry"
 
@@ -724,7 +732,7 @@ let make_unfold eref =
      poly = false;
      pat = None;
      name = PathHints [g];
-     code = Unfold_nth eref })
+     code = with_uid (Unfold_nth eref) })
 
 let make_extern pri pat tacast =
   let hdconstr = Option.map try_head_pattern pat in
@@ -733,7 +741,7 @@ let make_extern pri pat tacast =
      poly = false;
      pat = pat;
      name = PathAny;
-     code = Extern tacast })  
+     code = with_uid (Extern tacast) })  
 
 let make_mode ref m = 
   let ty = Global.type_of_global_unsafe ref in
@@ -756,7 +764,7 @@ let make_trivial env sigma poly ?(name=PathAny) r =
 	      poly = poly;
               pat = Some (pi3 (Patternops.pattern_of_constr env ce.evd (clenv_type ce)));
 	      name = name;
-              code=Res_pf_THEN_trivial_fail(c,t,ctx) })
+              code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) })
 
 
 
@@ -771,7 +779,7 @@ let get_db dbname =
   try searchtable_map dbname
   with Not_found -> Hint_db.empty empty_transparent_state false
 
-let add_hint dbname hintlist = 
+let add_hint dbname hintlist =
   let db = get_db dbname in
   let db' = Hint_db.add_list hintlist db in
     searchtable_add (dbname,db')
@@ -837,34 +845,36 @@ let subst_autohint (subst, obj) =
   let subst_hint (k,data as hint) =
     let k' = Option.smartmap subst_key k in
     let pat' = Option.smartmap (subst_pattern subst) data.pat in
-    let code' = match data.code with
+    let code' = match data.code.obj with
       | Res_pf (c,t,ctx) ->
           let c' = subst_mps subst c in
           let t' = subst_mps subst t in
-          if c==c' && t'==t then data.code else Res_pf (c', t',ctx)
+          if c==c' && t'==t then data.code.obj else Res_pf (c', t',ctx)
       | ERes_pf (c,t,ctx) ->
           let c' = subst_mps subst c in
           let t' = subst_mps subst t in
-          if c==c' && t'==t then data.code else ERes_pf (c',t',ctx)
+          if c==c' && t'==t then data.code.obj else ERes_pf (c',t',ctx)
       | Give_exact (c,t,ctx) ->
           let c' = subst_mps subst c in
 	  let t' = subst_mps subst t in
-          if c==c' && t'== t then data.code else Give_exact (c',t',ctx)
+          if c==c' && t'== t then data.code.obj else Give_exact (c',t',ctx)
       | Res_pf_THEN_trivial_fail (c,t,ctx) ->
           let c' = subst_mps subst c in
           let t' = subst_mps subst t in
-          if c==c' && t==t' then data.code else Res_pf_THEN_trivial_fail (c',t',ctx)
+          if c==c' && t==t' then data.code.obj else Res_pf_THEN_trivial_fail (c',t',ctx)
       | Unfold_nth ref ->
           let ref' = subst_evaluable_reference subst ref in
-          if ref==ref' then data.code else Unfold_nth ref'
+          if ref==ref' then data.code.obj else Unfold_nth ref'
       | Extern tac ->
 	  let tac' = Tacsubst.subst_tactic subst tac in
-	  if tac==tac' then data.code else Extern tac'
+	  if tac==tac' then data.code.obj else Extern tac'
     in
     let name' = subst_path_atom subst data.name in
+    let uid' = subst_kn subst data.code.uid in
     let data' =
-      if data.pat==pat' && data.name == name' && data.code==code' then data
-      else { data with pat = pat'; name = name'; code = code' }
+      if data.code.uid == uid' && data.pat == pat' &&
+        data.name == name' && data.code.obj == code' then data
+      else { data with pat = pat'; name = name'; code = { obj = code'; uid = uid' } }
     in
     if k' == k && data' == data then hint else (k',data')
   in
@@ -1146,8 +1156,7 @@ let make_db_list dbnames =
 (*                    Functions for printing the hints                    *)
 (**************************************************************************)
 
-let pr_hint =
-  function
+let pr_hint h = match h.obj with
   | Res_pf (c,clenv) -> (str"apply " ++ pr_constr c)
   | ERes_pf (c,clenv) -> (str"eapply " ++ pr_constr c)
   | Give_exact (c,clenv) -> (str"exact " ++ pr_constr c)
-- 
cgit v1.2.3


From e0a245daa30a3204ee487fe6f8d20a0674a2398c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 11 May 2015 18:34:00 +0200
Subject: Adding an option Loose Hint Behavior to handle hints loaded but not
 imported.

It accepts three distinct flags:
- "Lax", which is the default one, sets the old behaviour, i.e. a non-imported
hint behaves the same as an imported one.
- "Warn" outputs a warning when a non-imported hint is used. Note that this is
an over-approximation, because a hint may be triggered by an eauto run that
will eventually fail and backtrack.
- "Strict" changes the behaviour of an unloaded hint to the one of the fail
tactic, allowing to emulate the hopefully future import-scoped hint mechanism.
---
 tactics/hints.ml | 80 +++++++++++++++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 73 insertions(+), 7 deletions(-)

(limited to 'tactics')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 5a5be1cbc5..ae45aabd0b 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -112,8 +112,29 @@ type full_hint = hint with_metadata
 type hint_entry = global_reference option * 
   (constr * types * Univ.universe_context_set) hint_ast with_uid with_metadata
 
-let run_hint tac k = k tac.obj
-let repr_hint h = h.obj
+type import_level = [ `LAX | `WARN | `STRICT ]
+
+let warn_hint : import_level ref = ref `LAX
+let read_warn_hint () = match !warn_hint with
+| `LAX -> "Lax"
+| `WARN -> "Warn"
+| `STRICT -> "Strict"
+
+let write_warn_hint = function
+| "Lax" -> warn_hint := `LAX
+| "Warn" -> warn_hint := `WARN
+| "Strict" -> warn_hint := `STRICT
+| _ -> error "Only the following flags are accepted: Lax, Warn, Strict."
+
+let _ =
+  Goptions.declare_string_option
+    { Goptions.optsync  = true;
+      Goptions.optdepr  = false;
+      Goptions.optname  = "behavior of non-imported hints";
+      Goptions.optkey   = ["Loose"; "Hint"; "Behavior"];
+      Goptions.optread  = read_warn_hint;
+      Goptions.optwrite = write_warn_hint;
+    }
 
 let fresh_key =
   let id = Summary.ref ~name:"HINT-COUNTER" 0 in
@@ -592,6 +613,7 @@ let auto_init_db =
        Hintdbmap.empty)
 
 let searchtable : hint_db_table = ref auto_init_db
+let statustable = ref KNmap.empty
 
 let searchtable_map name =
   Hintdbmap.find name !searchtable
@@ -615,9 +637,10 @@ let add_hints_init f =
   let init = !hints_init in
   hints_init := (fun () -> init (); f ())
 
-let init     () = searchtable := auto_init_db; !hints_init ()
-let freeze   _ = !searchtable
-let unfreeze fs = searchtable := fs
+let init     () =
+  searchtable := auto_init_db; statustable := KNmap.empty; !hints_init ()
+let freeze   _ = (!searchtable, !statustable)
+let unfreeze (fs, st) = searchtable := fs; statustable := st
 
 let _ = Summary.declare_summary "search"
 	  { Summary.freeze_function   = freeze;
@@ -780,6 +803,14 @@ let get_db dbname =
   with Not_found -> Hint_db.empty empty_transparent_state false
 
 let add_hint dbname hintlist =
+  let check (_, h) =
+    let () = if KNmap.mem h.code.uid !statustable then
+      error "Conflicting hint keys. This can happen when including \
+      twice the same module."
+    in
+    statustable := KNmap.add h.code.uid false !statustable
+  in
+  let () = List.iter check hintlist in
   let db = get_db dbname in
   let db' = Hint_db.add_list hintlist db in
     searchtable_add (dbname,db')
@@ -824,7 +855,7 @@ type hint_obj = {
   hint_action : hint_action;
 }
 
-let cache_autohint (_, h) =
+let load_autohint _ (kn, h) =
   let name = h.hint_name in
   match h.hint_action with
   | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b)
@@ -834,6 +865,16 @@ let cache_autohint (_, h) =
   | AddCut path -> add_cut name path
   | AddMode (l, m) -> add_mode name l m
 
+let open_autohint i (kn, h) =
+  if Int.equal i 1 then match h.hint_action with
+  | AddHints hints ->
+    let add (_, hint) = statustable := KNmap.add hint.code.uid true !statustable in
+    List.iter add hints
+  | _ -> ()
+
+let cache_autohint (kn, obj) =
+  load_autohint 1 (kn, obj); open_autohint 1 (kn, obj)
+
 let subst_autohint (subst, obj) =
   let subst_key gr =
     let (lab'', elab') = subst_global subst gr in
@@ -906,7 +947,8 @@ let classify_autohint obj =
 let inAutoHint : hint_obj -> obj =
   declare_object {(default_object "AUTOHINT") with
                     cache_function = cache_autohint;
-		    load_function = (fun _ -> cache_autohint);
+		    load_function = load_autohint;
+		    open_function = open_autohint;
 		    subst_function = subst_autohint;
 		    classify_function = classify_autohint; }
 
@@ -1275,3 +1317,27 @@ let pr_searchtable () =
   in
   Hintdbmap.fold fold !searchtable (mt ())
 
+let print_mp mp =
+  try
+    let qid = Nametab.shortest_qualid_of_module mp in
+    str " from "  ++ pr_qualid qid
+  with Not_found -> mt ()
+
+let is_imported h = try KNmap.find h.uid !statustable with Not_found -> true
+
+let warn h x =
+  let hint = pr_hint h in
+  let (mp, _, _) = KerName.repr h.uid in
+  let () = msg_warning (str "Hint used but not imported: " ++ hint ++ print_mp mp) in
+  Proofview.tclUNIT x
+
+let run_hint tac k = match !warn_hint with
+| `LAX -> k tac.obj
+| `WARN ->
+  if is_imported tac then k tac.obj
+  else Proofview.tclBIND (k tac.obj) (fun x -> warn tac x)
+| `STRICT ->
+  if is_imported tac then k tac.obj
+  else Proofview.tclZERO (UserError ("", (str "Tactic failure.")))
+
+let repr_hint h = h.obj
-- 
cgit v1.2.3


From 3a7095f9f6a09a4461c2124b0020dfe37962de26 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 May 2015 17:47:24 +0200
Subject: Safer typing primitives.

Some functions from pretyping/typing.ml and their derivatives were potential
source of evarmap leaks, as they dropped their resulting evarmap. This commit
clarifies the situation by renaming them according to a unsafe_* scheme. Their
sound variant is likewise renamed to their old name. The following renamings
were made.

- Typing.type_of -> unsafe_type_of
- Typing.e_type_of -> type_of
- A new e_type_of function that matches the e_ prefix policy
- Tacmach.pf_type_of -> pf_unsafe_type_of
- A new safe pf_type_of function.

All uses of unsafe_* functions should be eventually eliminated.
---
 tactics/autorewrite.ml   |  4 ++--
 tactics/class_tactics.ml |  6 +++---
 tactics/contradiction.ml |  2 +-
 tactics/eauto.ml4        |  2 +-
 tactics/elim.ml          |  4 ++--
 tactics/eqdecide.ml      |  4 ++--
 tactics/equality.ml      | 22 ++++++++++-----------
 tactics/extratactics.ml4 |  4 ++--
 tactics/hints.ml         |  2 +-
 tactics/hipattern.ml4    |  2 +-
 tactics/inv.ml           |  6 +++---
 tactics/rewrite.ml       | 16 ++++++++--------
 tactics/tacinterp.ml     |  2 +-
 tactics/tacticals.ml     |  4 ++--
 tactics/tactics.ml       | 50 ++++++++++++++++++++++++------------------------
 15 files changed, 65 insertions(+), 65 deletions(-)

(limited to 'tactics')

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index ad8164fa64..2b3fadf7fa 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -263,7 +263,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
       try
 	let others,(c1,c2) = split_last_two args in
 	let ty1, ty2 =
-	  Typing.type_of env eqclause.evd c1, Typing.type_of env eqclause.evd c2
+	  Typing.unsafe_type_of env eqclause.evd c1, Typing.unsafe_type_of env eqclause.evd c2
 	in
 (* 	  if not (evd_convertible env eqclause.evd ty1 ty2) then None *)
 (* 	  else *)
@@ -281,7 +281,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
 	| None -> None
 
 let find_applied_relation metas loc env sigma c left2right =
-  let ctype = Typing.type_of env sigma c in
+  let ctype = Typing.unsafe_type_of env sigma c in
     match decompose_applied_relation metas env sigma c ctype left2right with
     | Some c -> c
     | None ->
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 6ea25269cf..ef78a953ac 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -149,7 +149,7 @@ let e_give_exact flags poly (c,clenv) gl =
 	c, {gl with sigma = clenv'.evd}
     else c, gl
   in
-  let t1 = pf_type_of gl c in
+  let t1 = pf_unsafe_type_of gl c in
     tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl
 
 let unify_e_resolve poly flags (c,clenv) gls =
@@ -168,7 +168,7 @@ let unify_resolve poly flags (c,clenv) gls =
 let clenv_of_prods poly nprods (c, clenv) gls =
   if poly || Int.equal nprods 0 then Some clenv
   else
-    let ty = pf_type_of gls c in
+    let ty = pf_unsafe_type_of gls c in
     let diff = nb_prod ty - nprods in
       if Pervasives.(>=) diff 0 then
         (* Was Some clenv... *)
@@ -842,6 +842,6 @@ let is_ground c gl =
 let autoapply c i gl =
   let flags = auto_unif_flags Evar.Set.empty 
     (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in
-  let cty = pf_type_of gl c in
+  let cty = pf_unsafe_type_of gl c in
   let ce = mk_clenv_from gl (c,cty) in
   unify_e_resolve false flags (c,ce) gl
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index c03710e911..22f218b4fb 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -90,7 +90,7 @@ let contradiction_term (c,lbind as cl) =
   Proofview.Goal.nf_enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
-    let type_of = Tacmach.New.pf_type_of gl in
+    let type_of = Tacmach.New.pf_unsafe_type_of gl in
     let typ = type_of c in
     let _, ccl = splay_prod env sigma typ in
     if is_empty_type ccl then
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 50925ecde6..34f87c6cf0 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -33,7 +33,7 @@ DECLARE PLUGIN "eauto"
 
 let eauto_unif_flags = auto_flags_of_state full_transparent_state
 
-let e_give_exact ?(flags=eauto_unif_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in
+let e_give_exact ?(flags=eauto_unif_flags) c gl = let t1 = (pf_unsafe_type_of gl c) and t2 = pf_concl gl in
   if occur_existential t1 || occur_existential t2 then
      tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl
   else Proofview.V82.of_tactic (exact_check c) gl
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 3cb4fa9c4c..4841d2c252 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -85,7 +85,7 @@ let up_to_delta = ref false (* true *)
 
 let general_decompose recognizer c =
   Proofview.Goal.enter begin fun gl ->
-  let type_of = pf_type_of gl in
+  let type_of = pf_unsafe_type_of gl in
   let typc = type_of c in
   tclTHENS (cut typc)
     [ tclTHEN (intro_using tmphyp_name)
@@ -139,7 +139,7 @@ let induction_trailer abs_i abs_j bargs =
     (onLastHypId
        (fun id ->
           Proofview.Goal.nf_enter begin fun gl ->
-	  let idty = pf_type_of gl (mkVar id) in
+	  let idty = pf_unsafe_type_of gl (mkVar id) in
 	  let fvty = global_vars (pf_env gl) idty in
 	  let possible_bring_hyps =
 	    (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 2ee4bf8e12..a5d68e19bd 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -133,7 +133,7 @@ let match_eqdec c =
 
 let solveArg eqonleft op a1 a2 tac =
   Proofview.Goal.enter begin fun gl ->
-  let rectype = pf_type_of gl a1 in
+  let rectype = pf_unsafe_type_of gl a1 in
   let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in
   let subtacs =
     if eqonleft then [eqCase tac;diseqCase eqonleft;default_auto]
@@ -203,7 +203,7 @@ let decideEquality rectype =
 
 let compare c1 c2 =
   Proofview.Goal.enter begin fun gl ->
-  let rectype = pf_type_of gl c1 in
+  let rectype = pf_unsafe_type_of gl c1 in
   let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in
   (tclTHENS (cut decide)
             [(tclTHEN  intro
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 593b7e9ea0..fb7237e4b2 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -165,7 +165,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
   in List.map try_occ occs
 
 let instantiate_lemma gl c ty l l2r concl =
-  let ct = pf_type_of gl c in
+  let ct = pf_unsafe_type_of gl c in
   let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
   let eqclause = pf_apply Clenv.make_clenv_binding gl (c,t) l in
    [eqclause]
@@ -944,7 +944,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
 
 let onEquality with_evars tac (c,lbindc) =
   Proofview.Goal.nf_enter begin fun gl ->
-  let type_of = pf_type_of gl in
+  let type_of = pf_unsafe_type_of gl in
   let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in
   let t = type_of c in
   let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in
@@ -1019,7 +1019,7 @@ let find_sigma_data env s = build_sigma_type ()
 let make_tuple env sigma (rterm,rty) lind =
   assert (dependent (mkRel lind) rty);
   let sigdata = find_sigma_data env (get_sort_of env sigma rty) in
-  let sigma, a = e_type_of ~refresh:true env sigma (mkRel lind) in
+  let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in
   let (na,_,_) = lookup_rel lind env in
   (* We move [lind] to [1] and lift other rels > [lind] by 1 *)
   let rty = lift (1-lind) (liftn lind (lind+1) rty) in
@@ -1053,7 +1053,7 @@ let minimal_free_rels_rec env sigma =
   let rec minimalrec_free_rels_rec prev_rels (c,cty) =
     let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in
     let combined_rels = Int.Set.union prev_rels direct_rels in
-    let folder rels i = snd (minimalrec_free_rels_rec rels (c, type_of env sigma (mkRel i)))
+    let folder rels i = snd (minimalrec_free_rels_rec rels (c, unsafe_type_of env sigma (mkRel i)))
     in (cty, List.fold_left folder combined_rels (Int.Set.elements (Int.Set.diff direct_rels prev_rels)))
   in minimalrec_free_rels_rec Int.Set.empty
 
@@ -1099,7 +1099,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
   let rec sigrec_clausal_form siglen p_i =
     if Int.equal siglen 0 then
       (* is the default value typable with the expected type *)
-      let dflt_typ = type_of env sigma dflt in
+      let dflt_typ = unsafe_type_of env sigma dflt in
       try
 	let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in
 	let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in
@@ -1118,7 +1118,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
           (destEvar ev)
       with
 	| Some w ->
-            let w_type = type_of env sigma w in
+            let w_type = unsafe_type_of env sigma w in
             if Evarconv.e_cumul env evdref w_type a then
 	      let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in
               applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
@@ -1200,7 +1200,7 @@ let make_iterated_tuple env sigma dflt (z,zty) =
     sigma, (tuple,tuplety,dfltval)
 
 let rec build_injrec env sigma dflt c = function
-  | [] -> make_iterated_tuple env sigma dflt (c,type_of env sigma c)
+  | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma c)
   | ((sp,cnum),argnum)::l ->
     try
       let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
@@ -1253,7 +1253,7 @@ let inject_if_homogenous_dependent_pair ty =
     if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind) &&
       pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
     Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"];
-    let new_eq_args = [|pf_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
+    let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
     let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
       ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
     let c, eff = find_scheme (!eq_dec_scheme_kind_name()) (Univ.out_punivs ind) in
@@ -1293,7 +1293,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
       let injfun = mkNamedLambda e t injbody in
       let sigma,congr = Evd.fresh_global env sigma eq.congr in
       let pf = applist(congr,[t;resty;injfun;t1;t2]) in
-      let sigma, pf_typ = Typing.e_type_of env sigma pf in
+      let sigma, pf_typ = Typing.type_of env sigma pf in
       let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
       let pf = Clenvtac.clenv_value_cast_meta inj_clause in
       let ty = simplify_args env sigma (clenv_type inj_clause) in
@@ -1460,8 +1460,8 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   (* Simulate now the normalisation treatment made by Logic.mk_refgoals *)
   let expected_goal = nf_betaiota sigma expected_goal in
   (* Retype to get universes right *)
-  let sigma, expected_goal_ty = Typing.e_type_of env sigma expected_goal in
-  let sigma, _ = Typing.e_type_of env sigma body in
+  let sigma, expected_goal_ty = Typing.type_of env sigma expected_goal in
+  let sigma, _ = Typing.type_of env sigma body in
     sigma,body,expected_goal
 
 (* Like "replace" but decompose dependent equalities                      *)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index f217cda894..177be2c205 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -704,7 +704,7 @@ let refl_equal =
   call it before it is defined. *)
 let  mkCaseEq a  : unit Proofview.tactic =
   Proofview.Goal.nf_enter begin fun gl ->
-    let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g a) gl in
+    let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in
        Tacticals.New.tclTHENLIST
          [Proofview.V82.tactic (Tactics.Simple.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]);
           Proofview.Goal.nf_enter begin fun gl ->
@@ -755,7 +755,7 @@ let destauto t =
 
 let destauto_in id = 
   Proofview.Goal.nf_enter begin fun gl ->
-  let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g (mkVar id)) gl in
+  let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (mkVar id)) gl in
 (*  Pp.msgnl (Printer.pr_lconstr (mkVar id)); *)
 (*  Pp.msgnl (Printer.pr_lconstr (ctype)); *)
   destauto ctype
diff --git a/tactics/hints.ml b/tactics/hints.ml
index ae45aabd0b..0df1a35c62 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -780,7 +780,7 @@ let make_mode ref m =
 let make_trivial env sigma poly ?(name=PathAny) r =
   let c,ctx = fresh_global_or_constr env sigma poly r in
   let sigma = Evd.merge_context_set univ_flexible sigma ctx in
-  let t = hnf_constr env sigma (type_of env sigma c) in
+  let t = hnf_constr env sigma (unsafe_type_of env sigma c) in
   let hd = head_of_constr_reference (head_constr t) in
   let ce = mk_clenv_from_env env sigma None (c,t) in
   (Some hd, { pri=1;
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 4b94f420ba..95f3af57e2 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -411,7 +411,7 @@ let find_eq_data eqn = (* fails with PatternMatchingFailure *)
 
 let extract_eq_args gl = function
   | MonomorphicLeibnizEq (e1,e2) ->
-      let t = pf_type_of gl e1 in (t,e1,e2)
+      let t = pf_unsafe_type_of gl e1 in (t,e1,e2)
   | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2)
   | HeterogenousEq (t1,e1,t2,e2) ->
       if pf_conv_x gl t1 t2 then (t1,e1,e2)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 5502356fbf..ef115aea0e 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -123,13 +123,13 @@ let make_inv_predicate env evd indf realargs id status concl =
         let refl_term = eqdata.Coqlib.refl in
 	let refl_term = Evarutil.evd_comb1 (Evd.fresh_global env) evd refl_term in
         let refl = mkApp (refl_term, [|eqnty; rhs|]) in
-	let _ = Evarutil.evd_comb1 (Typing.e_type_of env) evd refl in
+	let _ = Evarutil.evd_comb1 (Typing.type_of env) evd refl in
         let args = refl :: args in
         build_concl eqns args (succ n) restlist
   in
   let (newconcl, args) = build_concl [] [] 0 realargs in
   let predicate = it_mkLambda_or_LetIn_name env newconcl hyps in
-  let _ = Evarutil.evd_comb1 (Typing.e_type_of env) evd predicate in
+  let _ = Evarutil.evd_comb1 (Typing.type_of env) evd predicate in
   (* OK - this predicate should now be usable by res_elimination_then to
      do elimination on the conclusion. *)
   predicate, args
@@ -437,7 +437,7 @@ let raw_inversion inv_kind id status names =
     let concl = Proofview.Goal.concl gl in
     let c = mkVar id in
     let (ind, t) =
-      try pf_apply Tacred.reduce_to_atomic_ind gl (pf_type_of gl c)
+      try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c)
       with UserError _ ->
         let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in
         Errors.errorlabstrm "" msg
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index d487317736..6d26e91c68 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -381,7 +381,7 @@ end
 
 let type_app_poly env env evd f args =
   let evars, c = app_poly_nocheck env evd f args in
-  let evd', t = Typing.e_type_of env (goalevars evars) c in
+  let evd', t = Typing.type_of env (goalevars evars) c in
     (evd', cstrevars evars), c
 
 module PropGlobal = struct
@@ -472,7 +472,7 @@ let rec decompose_app_rel env evd t =
   | App (f, [||]) -> assert false
   | App (f, [|arg|]) ->
     let (f', argl, argr) = decompose_app_rel env evd arg in
-    let ty = Typing.type_of env evd argl in
+    let ty = Typing.unsafe_type_of env evd argl in
     let f'' = mkLambda (Name default_dependent_ident, ty,
       mkLambda (Name (Id.of_string "y"), lift 1 ty,
         mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |])))
@@ -747,7 +747,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
     let morphargs, morphobjs = Array.chop first args in
     let morphargs', morphobjs' = Array.chop first args' in
     let appm = mkApp(m, morphargs) in
-    let appmtype = Typing.type_of env (goalevars evars) appm in
+    let appmtype = Typing.unsafe_type_of env (goalevars evars) appm in
     let cstrs = List.map 
       (Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf)) 
       (Array.to_list morphobjs') 
@@ -1738,7 +1738,7 @@ let declare_projection n instance_id r =
   let poly = Global.is_polymorphic r in
   let ty = Retyping.get_type_of (Global.env ()) Evd.empty c in
   let term = proper_projection c ty in
-  let typ = Typing.type_of (Global.env ()) Evd.empty term in
+  let typ = Typing.unsafe_type_of (Global.env ()) Evd.empty term in
   let ctx, typ = decompose_prod_assum typ in
   let typ =
     let n =
@@ -1771,7 +1771,7 @@ let build_morphism_signature m =
   let env = Global.env () in
   let m,ctx = Constrintern.interp_constr env Evd.empty m in
   let sigma = Evd.from_env ~ctx env in
-  let t = Typing.type_of env sigma m in
+  let t = Typing.unsafe_type_of env sigma m in
   let cstrs =
     let rec aux t =
       match kind_of_term t with
@@ -1798,7 +1798,7 @@ let build_morphism_signature m =
 
 let default_morphism sign m =
   let env = Global.env () in
-  let t = Typing.type_of env Evd.empty m in
+  let t = Typing.unsafe_type_of env Evd.empty m in
   let evars, _, sign, cstrs =
     PropGlobal.build_signature (Evd.empty, Evar.Set.empty) env t (fst sign) (snd sign)
   in
@@ -1994,7 +1994,7 @@ let setoid_proof ty fn fallback =
         try
           let rel, _, _ = decompose_app_rel env sigma concl in
           let evm = sigma in
-          let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in
+          let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.unsafe_type_of env evm rel)))) in
 	    (try init_setoid () with _ -> raise Not_found);
             fn env sigma car rel
         with e -> Proofview.tclZERO e
@@ -2053,7 +2053,7 @@ let setoid_transitivity c =
     
 let setoid_symmetry_in id =
   Proofview.V82.tactic (fun gl ->
-  let ctype = pf_type_of gl (mkVar id) in
+  let ctype = pf_unsafe_type_of gl (mkVar id) in
   let binders,concl = decompose_prod_assum ctype in
   let (equiv, args) = decompose_app concl in
   let rec split_last_two = function
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 7ce158fd1a..374c7c7364 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -734,7 +734,7 @@ let interp_may_eval f ist env sigma = function
 	    str "Unbound context identifier" ++ pr_id s ++ str"."))
   | ConstrTypeOf c ->
       let (sigma,c_interp) = f ist env sigma c in
-      Typing.e_type_of ~refresh:true env sigma c_interp
+      Typing.type_of ~refresh:true env sigma c_interp
   | ConstrTerm c ->
      try
 	f ist env sigma c
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 5ba53a7641..7d1cc3341c 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -598,7 +598,7 @@ module New = struct
     (** FIXME: evar leak. *)
     let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in
     (* applying elimination_scheme just a little modified *)
-    let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_type_of gl elim)) gl in
+    let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl elim)) gl in
     let indmv =
       match kind_of_term (last_arg elimclause.templval.Evd.rebus) with
       | Meta mv -> mv
@@ -651,7 +651,7 @@ module New = struct
 
   let elimination_then tac c =
     Proofview.Goal.nf_enter begin fun gl ->
-    let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
+    let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in
     let isrec,mkelim =
       match (Global.lookup_mind (fst (fst ind))).mind_record with
       | None -> true,gl_make_elim
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3038a95068..2791d7c484 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -158,7 +158,7 @@ let convert_concl ?(check=true) ty k =
     Proofview.Refine.refine ~unsafe:true begin fun sigma ->
       let sigma =
         if check then begin
-          ignore (Typing.type_of env sigma ty);
+          ignore (Typing.unsafe_type_of env sigma ty);
           let sigma,b = Reductionops.infer_conv env sigma ty conclty in
           if not b then error "Not convertible.";
           sigma
@@ -628,7 +628,7 @@ let change_on_subterm cv_pb deep t where env sigma c =
         env sigma c in
   if !mayneedglobalcheck then
     begin
-      try ignore (Typing.type_of env sigma c)
+      try ignore (Typing.unsafe_type_of env sigma c)
       with e when catchable_exception e ->
         error "Replacement would lead to an ill-typed term."
     end;
@@ -979,7 +979,7 @@ let cut c =
     let is_sort =
       try
         (** Backward compat: ensure that [c] is well-typed. *)
-        let typ = Typing.type_of env sigma c in
+        let typ = Typing.unsafe_type_of env sigma c in
         let typ = whd_betadeltaiota env sigma typ in
         match kind_of_term typ with
         | Sort _ -> true
@@ -1224,7 +1224,7 @@ let find_ind_eliminator ind s gl =
     evd, c
 
 let find_eliminator c gl =
-  let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_type_of gl c) in
+  let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in
   if is_nonrec ind then raise IsNonrec;
   let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in
     evd, {elimindex = None; elimbody = (c,NoBindings);
@@ -1639,7 +1639,7 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam
 
 let cut_and_apply c =
   Proofview.Goal.nf_enter begin fun gl ->
-    match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_type_of gl c)) with
+    match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with
       | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) ->
         let concl = Proofview.Goal.concl gl in
         let env = Tacmach.New.pf_env gl in
@@ -1672,7 +1672,7 @@ let exact_check c =
   let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
-  let sigma, ct = Typing.e_type_of env sigma c in
+  let sigma, ct = Typing.type_of env sigma c in
     Proofview.Unsafe.tclEVARS sigma <*>
       Tacticals.New.tclTHEN (convert_leq ct concl) (new_exact_no_check c)
   end
@@ -1821,7 +1821,7 @@ let specialize (c,lbind) g =
       let evd = Typeclasses.resolve_typeclasses (pf_env g) (project g) in
 	tclEVARS evd, nf_evar evd c
     else
-      let clause = pf_apply make_clenv_binding g (c,pf_type_of g c) lbind in
+      let clause = pf_apply make_clenv_binding g (c,pf_unsafe_type_of g c) lbind in
       let flags = { (default_unify_flags ()) with resolve_evars = true } in
       let clause = clenv_unify_meta_types ~flags clause in
       let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in
@@ -1841,11 +1841,11 @@ let specialize (c,lbind) g =
        | Var id when Id.List.mem id (pf_ids_of_hyps g) ->
 	   tclTHEN tac
 	     (tclTHENFIRST
-	       (fun g -> Proofview.V82.of_tactic (assert_before_replacing id (pf_type_of g term)) g)
+	       (fun g -> Proofview.V82.of_tactic (assert_before_replacing id (pf_unsafe_type_of g term)) g)
 	       (exact_no_check term)) g
        | _ -> tclTHEN tac
 	   (tclTHENLAST
-              (fun g -> Proofview.V82.of_tactic (cut (pf_type_of g term)) g)
+              (fun g -> Proofview.V82.of_tactic (cut (pf_unsafe_type_of g term)) g)
               (exact_no_check term)) g
 
 (* Keeping only a few hypotheses *)
@@ -1980,7 +1980,7 @@ let my_find_eq_data_decompose gl t =
 let intro_decomp_eq loc l thin tac id =
   Proofview.Goal.nf_enter begin fun gl ->
   let c = mkVar id in
-  let t = Tacmach.New.pf_type_of gl c in
+  let t = Tacmach.New.pf_unsafe_type_of gl c in
   let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in
   match my_find_eq_data_decompose gl t with
   | Some (eq,u,eq_args) ->
@@ -1994,7 +1994,7 @@ let intro_decomp_eq loc l thin tac id =
 let intro_or_and_pattern loc bracketed ll thin tac id =
   Proofview.Goal.enter begin fun gl ->
   let c = mkVar id in
-  let t = Tacmach.New.pf_type_of gl c in
+  let t = Tacmach.New.pf_unsafe_type_of gl c in
   let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in
   let nv = constructors_nrealargs ind in
   let ll = fix_empty_or_and_pattern (Array.length nv) ll in
@@ -2013,7 +2013,7 @@ let rewrite_hyp assert_style l2r id =
   let clear_var_and_eq c = tclTHEN (clear [id]) (clear [destVar c]) in
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
-    let type_of = Tacmach.New.pf_type_of gl in
+    let type_of = Tacmach.New.pf_unsafe_type_of gl in
     let whd_betadeltaiota = Tacmach.New.pf_apply whd_betadeltaiota gl in
     let t = whd_betadeltaiota (type_of (mkVar id)) in
     match match_with_equality_type t with
@@ -2290,7 +2290,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
           let eq = applist (eq,args) in
           let refl = applist (refl, [t;mkVar id]) in
 	  let term = mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)) in
-	  let sigma, _ = Typing.e_type_of env sigma term in
+	  let sigma, _ = Typing.type_of env sigma term in
             sigma, term,
             Tacticals.New.tclTHEN
 	      (intro_gen (NamingMustBe (loc,heq)) (decode_hyp lastlhyp) true false)
@@ -2376,7 +2376,7 @@ let forward b usetac ipat c =
   match usetac with
   | None ->
       Proofview.Goal.enter begin fun gl ->
-      let t = Tacmach.New.pf_type_of gl  c in
+      let t = Tacmach.New.pf_unsafe_type_of gl  c in
       Tacticals.New.tclTHENFIRST (assert_as true ipat t)
 	(Proofview.V82.tactic (exact_no_check c))
       end
@@ -2459,7 +2459,7 @@ let generalize_goal_gen env ids i ((occs,c,b),na) t (cl,evd) =
     mkProd_or_LetIn (na,b,t) cl', evd'
 
 let generalize_goal gl i ((occs,c,b),na as o) cl =
-  let t = pf_type_of gl c in
+  let t = pf_unsafe_type_of gl c in
   let env = pf_env gl in
     generalize_goal_gen env (pf_ids_of_hyps gl) i o t cl
 
@@ -2520,7 +2520,7 @@ let new_generalize_gen_let lconstr =
     let (newcl, sigma), args =
       List.fold_right_i 
 	(fun i ((_,c,b),_ as o) (cl, args) ->
-	  let t = Tacmach.New.pf_type_of gl c in
+	  let t = Tacmach.New.pf_unsafe_type_of gl c in
 	  let args = if Option.is_empty b then c :: args else args in
 	    generalize_goal_gen env ids i o t cl, args)
 	0 lconstr ((concl, sigma), [])
@@ -2797,7 +2797,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
             let id = match kind_of_term c with
             | Var id -> id
             | _ ->
-            let type_of = Tacmach.New.pf_type_of gl in
+            let type_of = Tacmach.New.pf_unsafe_type_of gl in
             id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
             let x = fresh_id_in_env avoid id env in
 	    Tacticals.New.tclTHEN
@@ -3201,7 +3201,7 @@ let abstract_args gl generalize_vars dep id defined f args =
       let rel, c = Reductionops.splay_prod_n env sigma 1 prod in
 	List.hd rel, c
     in
-    let argty = pf_type_of gl arg in
+    let argty = pf_unsafe_type_of gl arg in
     let ty = (* refresh_universes_strict *) ty in
     let lenctx = List.length ctx in
     let liftargty = lift lenctx argty in
@@ -3242,7 +3242,7 @@ let abstract_args gl generalize_vars dep id defined f args =
   in
     if dogen then
       let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env =
-	Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args'
+	Array.fold_left aux (pf_unsafe_type_of gl f',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args'
       in
       let args, refls = List.rev args, List.rev refls in
       let vars =
@@ -3566,13 +3566,13 @@ let guess_elim isrec dep s hyp0 gl =
 	Tacmach.New.pf_apply build_case_analysis_scheme gl mind true s
       else
 	Tacmach.New.pf_apply build_case_analysis_scheme_default gl mind s in
-  let elimt = Tacmach.New.pf_type_of gl elimc in
+  let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in
     evd, ((elimc, NoBindings), elimt), mkIndU mind
 
 let given_elim hyp0 (elimc,lbind as e) gl =
   let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
   let ind_type_guess,_ = decompose_app ((strip_prod tmptyp0)) in
-  Proofview.Goal.sigma gl, (e, Tacmach.New.pf_type_of gl elimc), ind_type_guess
+  Proofview.Goal.sigma gl, (e, Tacmach.New.pf_unsafe_type_of gl elimc), ind_type_guess
 
 type scheme_signature =
     (Id.t list * (elim_arg_kind * bool * Id.t) list) array
@@ -3604,7 +3604,7 @@ let get_elim_signature elim hyp0 gl =
   compute_elim_signature (given_elim hyp0 elim gl) hyp0
 
 let is_functional_induction elimc gl =
-  let scheme = compute_elim_sig ~elimc (Tacmach.New.pf_type_of gl (fst elimc)) in
+  let scheme = compute_elim_sig ~elimc (Tacmach.New.pf_unsafe_type_of gl (fst elimc)) in
   (* The test is not safe: with non-functional induction on non-standard
      induction scheme, this may fail *)
   Option.is_empty scheme.indarg
@@ -3963,7 +3963,7 @@ let induction_gen_l isrec with_evars elim names lc =
 
 	    | _ ->
                 Proofview.Goal.enter begin fun gl ->
-                let type_of = Tacmach.New.pf_type_of gl in
+                let type_of = Tacmach.New.pf_unsafe_type_of gl in
                 let x =
 		  id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
 
@@ -4225,7 +4225,7 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make ()
 
 let symmetry_in id =
   Proofview.Goal.enter begin fun gl ->
-  let ctype = Tacmach.New.pf_type_of gl (mkVar id) in
+  let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in
   let sign,t = decompose_prod_assum ctype in
   Proofview.tclORELSE
     begin
@@ -4276,7 +4276,7 @@ let prove_transitivity hdcncl eq_kind t =
   | HeterogenousEq (typ1,c1,typ2,c2) ->
       let env = Proofview.Goal.env gl in
       let sigma = Proofview.Goal.sigma gl in
-      let type_of = Typing.type_of env sigma in
+      let type_of = Typing.unsafe_type_of env sigma in
       let typt = type_of t in
         (mkApp(hdcncl, [| typ1; c1; typt ;t |]),
          mkApp(hdcncl, [| typt; t; typ2; c2 |]))
-- 
cgit v1.2.3


From d91addb140ba7315d70c4599b0d058bef798ac1c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 May 2015 23:38:55 +0200
Subject: Fixing bug #4216:

Internal error: Anomaly: Uncaught exception Not_found. Please report.

An evarmap was lost because of an unsound typing primitive.
---
 tactics/equality.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index fb7237e4b2..ea74dc37ea 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -165,10 +165,10 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
   in List.map try_occ occs
 
 let instantiate_lemma gl c ty l l2r concl =
-  let ct = pf_unsafe_type_of gl c in
-  let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
-  let eqclause = pf_apply Clenv.make_clenv_binding gl (c,t) l in
-   [eqclause]
+  let sigma, ct = pf_type_of gl c in
+  let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma ct) with UserError _ -> ct in
+  let eqclause = Clenv.make_clenv_binding (pf_env gl) sigma (c,t) l in
+  [eqclause]
 
 let rewrite_conv_closed_core_unif_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
-- 
cgit v1.2.3