Merge v8.5 into trunk

Conflicts:
	tactics/eauto.ml4

(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)

21 files changed, 303 insertions, 202 deletions

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/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 3fafbe15a1..e1fe51656f 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... *)
@@ -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 =
@@ -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 bd55e6fb1e..b7dc7b4931 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -35,7 +35,7 @@ let eauto_unif_flags = auto_flags_of_state full_transparent_state
 
 let e_give_exact ?(flags=eauto_unif_flags) c =
   Proofview.Goal.nf_enter begin fun gl ->
-  let t1 = Tacmach.New.pf_type_of gl c in
+  let t1 = Tacmach.New.pf_unsafe_type_of gl c in
   let t2 = Tacmach.New.pf_concl gl in
   if occur_existential t1 || occur_existential t2 then
      Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (Proofview.V82.tactic (exact_no_check c))
@@ -182,8 +182,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 = run_auto_tactic t tac in
-       (tac, lazy (pr_autotactic t)))
+       let tac = run_hint t tac in
+       (tac, lazy (pr_hint t)))
   in
   List.map tac_of_hint hintl
 
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 f2860a2300..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_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;
@@ -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                      *)
@@ -1662,26 +1662,40 @@ 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
+    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
-    List.map_filter test hyps
+    List.rev (List.map_filter test hyps)
   in
 
   (* Second step: treat equations *)
@@ -1694,9 +1708,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 ->
@@ -1704,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 *)
 
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 f83aa56017..0df1a35c62 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,23 +92,64 @@ type hint_term =
   | IsGlobRef of global_reference
   | IsConstr of constr * Univ.universe_context_set
 
-type 'a auto_tactic = 'a auto_tactic_ast
+type 'a with_uid = {
+  obj : 'a;
+  uid : KerName.t;
+}
+
+type hint = (constr * clausenv) hint_ast with_uid
 
-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 *)
   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 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
-
-let run_auto_tactic tac k = k tac
-let repr_auto_tactic tac = tac
+  (constr * types * Univ.universe_context_set) hint_ast with_uid with_metadata
+
+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
+  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
@@ -125,7 +166,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 +194,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
@@ -175,21 +216,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 +275,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 +283,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 +501,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_gen_auto_tactic 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 +527,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
@@ -586,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
@@ -609,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;
@@ -632,6 +661,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 +678,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 +698,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 +709,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 +755,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 +764,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
@@ -749,14 +780,14 @@ 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;
 	      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 +802,15 @@ 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 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')
@@ -816,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)
@@ -826,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
@@ -837,34 +886,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
@@ -896,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; }
 
@@ -1146,8 +1198,7 @@ let make_db_list dbnames =
 (*                    Functions for printing the hints                    *)
 (**************************************************************************)
 
-let pr_autotactic =
-  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)
@@ -1163,11 +1214,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 ":" ++
@@ -1266,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
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 *)
 
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 60ce0e0dc3..6d26e91c68 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
@@ -380,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
@@ -452,7 +453,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;
@@ -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 |]) |])))
@@ -498,7 +498,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 +510,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 +584,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 +703,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
@@ -763,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') 
@@ -829,27 +813,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 +841,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 +1363,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 +1375,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 =
@@ -1755,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 =
@@ -1788,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
@@ -1815,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
@@ -1967,12 +1950,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
@@ -2011,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
@@ -2070,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/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
 
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index e8cb8c63bc..492b51f1a7 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 424bb142c7..7ee591cca7 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
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 |]))