Hints API using EConstr.

8 files changed, 162 insertions, 144 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 41b56bd3d0..2423ea8788 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -93,7 +93,7 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl =
         evd = Evd.map_metas map evd;
         env = Proofview.Goal.env gl;
       } in
-      clenv, map c
+      clenv, emap c
     else
       let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
       { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
@@ -115,7 +115,6 @@ let unify_resolve_gen poly = function
 let exact poly (c,clenv) =
   Proofview.Goal.enter { enter = begin fun gl ->
     let clenv', c = connect_hint_clenv poly c clenv gl in
-    let c = EConstr.of_constr c in
     Tacticals.New.tclTHEN
     (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
     (exact_check c)
@@ -141,7 +140,7 @@ let conclPattern concl pat tac =
     | None -> Proofview.tclUNIT Id.Map.empty
     | Some pat ->
 	try
-	  Proofview.tclUNIT (Constr_matching.matches env sigma pat (EConstr.of_constr concl))
+	  Proofview.tclUNIT (Constr_matching.matches env sigma pat concl)
 	with Constr_matching.PatternMatchingFailure ->
           Tacticals.New.tclZEROMSG (str "conclPattern")
   in
@@ -300,13 +299,13 @@ let flags_of_state st =
 let auto_flags_of_state st =
   auto_unif_flags_of full_transparent_state st false
 
-let hintmap_of secvars hdc concl =
+let hintmap_of sigma secvars hdc concl =
   match hdc with
   | None -> Hint_db.map_none ~secvars
   | Some hdc ->
-     if occur_existential Evd.empty (EConstr.of_constr concl) then (** FIXME *)
-       Hint_db.map_existential ~secvars hdc concl
-     else Hint_db.map_auto ~secvars hdc concl
+     if occur_existential sigma concl then
+       Hint_db.map_existential sigma ~secvars hdc concl
+     else Hint_db.map_auto sigma ~secvars hdc concl
 
 let exists_evaluable_reference env = function
   | EvalConstRef _ -> true
@@ -331,6 +330,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
   in
   Proofview.Goal.enter { enter = begin fun gl ->
     let concl = Tacmach.New.pf_nf_concl gl in
+    let concl = EConstr.of_constr concl in
     let sigma = Tacmach.New.project gl in
     let secvars = compute_secvars gl in
     Tacticals.New.tclFIRST
@@ -339,17 +339,17 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
              (trivial_resolve sigma dbg mod_delta db_list local_db secvars concl)))
   end }
 
-and my_find_search_nodelta db_list local_db secvars hdc concl =
+and my_find_search_nodelta sigma db_list local_db secvars hdc concl =
   List.map (fun hint -> (None,hint))
-    (List.map_append (hintmap_of secvars hdc concl) (local_db::db_list))
+    (List.map_append (hintmap_of sigma secvars hdc concl) (local_db::db_list))
 
 and my_find_search mod_delta =
   if mod_delta then my_find_search_delta
   else my_find_search_nodelta
 
-and my_find_search_delta db_list local_db secvars hdc concl =
-  let f = hintmap_of secvars hdc concl in
-    if occur_existential Evd.empty (EConstr.of_constr concl) (** FIXME *) then
+and my_find_search_delta sigma db_list local_db secvars hdc concl =
+  let f = hintmap_of sigma secvars hdc concl in
+    if occur_existential sigma concl then
       List.map_append
 	(fun db ->
 	  if Hint_db.use_dn db then
@@ -371,8 +371,8 @@ and my_find_search_delta db_list local_db secvars hdc concl =
 	      match hdc with None -> Hint_db.map_none ~secvars db
 	      | Some hdc ->
 		  if (Id.Pred.is_empty ids && Cpred.is_empty csts)
-		  then Hint_db.map_auto ~secvars hdc concl db
-		  else Hint_db.map_existential ~secvars hdc concl db
+		  then Hint_db.map_auto sigma ~secvars hdc concl db
+		  else Hint_db.map_existential sigma ~secvars hdc concl db
 	    in auto_flags_of_state st, l
 	  in List.map (fun x -> (Some flags,x)) l)
       	(local_db::db_list)
@@ -414,7 +414,7 @@ and trivial_resolve sigma dbg mod_delta db_list local_db secvars cl =
     in
       List.map (tac_of_hint dbg db_list local_db cl)
 	(priority
-	    (my_find_search mod_delta db_list local_db secvars head cl))
+	    (my_find_search mod_delta sigma db_list local_db secvars head cl))
   with Not_found -> []
 
 (** The use of the "core" database can be de-activated by passing
@@ -460,7 +460,7 @@ let possible_resolve sigma dbg mod_delta db_list local_db secvars cl =
       with Bound -> None
     in
       List.map (tac_of_hint dbg db_list local_db cl)
-	(my_find_search mod_delta db_list local_db secvars head cl)
+	(my_find_search mod_delta sigma db_list local_db secvars head cl)
   with Not_found -> []
 
 let extend_local_db decl db gl =
@@ -491,6 +491,7 @@ let search d n mod_delta db_list local_db =
 	  (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
 	     ( Proofview.Goal.enter { enter = begin fun gl ->
                let concl = Tacmach.New.pf_nf_concl gl in
+               let concl = EConstr.of_constr concl in
                let sigma = Tacmach.New.project gl in
                let secvars = compute_secvars gl in
 	       let d' = incr_dbg d in
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 06048ac1c5..403be9e1cc 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -23,7 +23,7 @@ val default_search_depth : int ref
 val auto_flags_of_state : transparent_state -> Unification.unify_flags
 
 val connect_hint_clenv : polymorphic -> raw_hint -> clausenv ->
-  ('a, 'r) Proofview.Goal.t -> clausenv * constr
+  ('a, 'r) Proofview.Goal.t -> clausenv * EConstr.constr
 
 (** Try unification with the precompiled clause, then use registered Apply *)
 val unify_resolve : polymorphic -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic
@@ -33,7 +33,7 @@ val unify_resolve : polymorphic -> Unification.unify_flags -> (raw_hint * clause
    [Pattern.somatches], then replace [?1] [?2] metavars in tacast by the
    right values to build a tactic *)
 
-val conclPattern : constr -> constr_pattern option -> Genarg.glob_generic_argument -> unit Proofview.tactic
+val conclPattern : EConstr.constr -> constr_pattern option -> Genarg.glob_generic_argument -> unit Proofview.tactic
 
 (** The Auto tactic *)
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 02211efd6e..8ecdd01f23 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -217,6 +217,7 @@ let auto_unif_flags freeze st =
 }
 
 let e_give_exact flags poly (c,clenv) gl =
+  let open EConstr in
   let (c, _, _) = c in
   let c, gl =
     if poly then
@@ -226,7 +227,6 @@ let e_give_exact flags poly (c,clenv) gl =
         c, {gl with sigma = evd}
     else c, gl
   in
-  let c = EConstr.of_constr c in
   let t1 = pf_unsafe_type_of gl c in
   let t1 = EConstr.of_constr t1 in
   Proofview.V82.of_tactic (Clenvtac.unify ~flags t1 <*> exact_no_check c) gl
@@ -245,6 +245,7 @@ let unify_resolve poly flags = { enter = begin fun gls (c,_,clenv) ->
 
 (** Application of a lemma using [refine] instead of the old [w_unify] *)
 let unify_resolve_refine poly flags =
+  let open EConstr in
   let open Clenv in
   { enter = begin fun gls ((c, t, ctx),n,clenv) ->
     let env = Proofview.Goal.env gls in
@@ -262,9 +263,6 @@ let unify_resolve_refine poly flags =
           let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
           sigma, c, t
       in
-      let open EConstr in
-      let ty = EConstr.of_constr ty in
-      let term = EConstr.of_constr term in
       let sigma', cl = Clenv.make_evar_clause env sigma ?len:n ty in
       let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in
       let sigma' =
@@ -285,7 +283,6 @@ let clenv_of_prods poly nprods (c, clenv) gl =
   let (c, _, _) = c in
   if poly || Int.equal nprods 0 then Some (None, clenv)
   else
-    let c = EConstr.of_constr c in
     let sigma = Tacmach.New.project gl in
     let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in
     let ty = EConstr.of_constr ty in
@@ -313,7 +310,7 @@ let matches_pattern concl pat =
     | None -> Proofview.tclUNIT ()
     | Some pat ->
        let sigma = Sigma.to_evar_map sigma in
-       if Constr_matching.is_matching env sigma pat (EConstr.of_constr concl) then
+       if Constr_matching.is_matching env sigma pat concl then
          Proofview.tclUNIT ()
        else
          Tacticals.New.tclZEROMSG (str "conclPattern")
@@ -367,7 +364,7 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars =
     Proofview.Goal.nf_enter { enter =
     begin fun gl ->
     let tacs = e_trivial_resolve db_list local_db secvars only_classes
-                                 (project gl) (pf_concl gl) in
+                                 (project gl) (EConstr.of_constr (pf_concl gl)) in
       tclFIRST (List.map (fun (x,_,_,_,_) -> x) tacs)
     end}
   in
@@ -379,13 +376,13 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars =
 
 and e_my_find_search db_list local_db secvars hdc complete only_classes sigma concl =
   let open Proofview.Notations in
-  let prods, concl = decompose_prod_assum concl in
+  let prods, concl = EConstr.decompose_prod_assum sigma concl in
   let nprods = List.length prods in
   let freeze =
     try
       let cl = Typeclasses.class_info (fst hdc) in
         if cl.cl_strict then
-          Evd.evars_of_term concl
+          Evarutil.undefined_evars_of_term sigma concl
         else Evar.Set.empty
     with e when CErrors.noncritical e -> Evar.Set.empty
   in
@@ -394,8 +391,8 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
       (fun db ->
         let tacs =
           if Hint_db.use_dn db then (* Using dnet *)
-            Hint_db.map_eauto secvars hdc concl db
-          else Hint_db.map_existential secvars hdc concl db
+            Hint_db.map_eauto sigma secvars hdc concl db
+          else Hint_db.map_existential sigma secvars hdc concl db
         in
         let flags = auto_unif_flags freeze (Hint_db.transparent_state db) in
           List.map (fun x -> (flags, x)) tacs)
@@ -481,7 +478,7 @@ let catchable = function
 let pr_depth l = prlist_with_sep (fun () -> str ".") int (List.rev l)
 
 let is_Prop env sigma concl =
-  let ty = Retyping.get_type_of env sigma (EConstr.of_constr concl) in
+  let ty = Retyping.get_type_of env sigma concl in
   match kind_of_term ty with
   | Sort (Prop Null) -> true
   | _ -> false
@@ -542,9 +539,10 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
                else false
   in
   let is_class = iscl env cty in
+  let cty = EConstr.of_constr cty in
   let keep = not only_classes || is_class in
     if keep then
-      let c = mkVar id in
+      let c = EConstr.mkVar id in
       let name = PathHints [VarRef id] in
       let hints =
         if is_class then
@@ -552,7 +550,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
             (List.map_append
                (fun (path,pri, c) -> make_resolves env sigma ~name:(PathHints path)
                   (true,false,Flags.is_verbose()) pri false
-                 (IsConstr (c,Univ.ContextSet.empty)))
+                 (IsConstr (EConstr.of_constr c,Univ.ContextSet.empty)))
                hints)
         else []
       in
@@ -674,17 +672,16 @@ module V85 = struct
 
   let needs_backtrack env evd oev concl =
     if Option.is_empty oev || is_Prop env evd concl then
-      occur_existential evd (EConstr.of_constr concl)
+      occur_existential evd concl
     else true
 
   let hints_tac hints sk fk {it = gl,info; sigma = s} =
     let env = Goal.V82.env s gl in
     let concl = Goal.V82.concl s gl in
-    let concl = EConstr.Unsafe.to_constr concl in
     let tacgl = {it = gl; sigma = s;} in
     let secvars = secvars_of_hyps (Environ.named_context_of_val (Goal.V82.hyps s gl)) in
     let poss = e_possible_resolve hints info.hints secvars info.only_classes s concl in
-    let unique = is_unique env s (EConstr.of_constr concl) in
+    let unique = is_unique env s concl in
     let rec aux i foundone = function
       | (tac, _, extern, name, pp) :: tl ->
          let derivs = path_derivate info.auto_cut name in
@@ -749,7 +746,7 @@ module V85 = struct
              let fk' =
                (fun e ->
                  let do_backtrack =
-                   if unique then occur_existential s' (EConstr.of_constr concl)
+                   if unique then occur_existential s' concl
                    else if info.unique then true
                    else if List.is_empty gls' then
                      needs_backtrack env s' info.is_evar concl
@@ -770,7 +767,7 @@ module V85 = struct
          if foundone == None && !typeclasses_debug > 0 then
            Feedback.msg_debug
              (pr_depth info.auto_depth ++ str": no match for " ++
-                Printer.pr_constr_env (Goal.V82.env s gl) s concl ++
+                Printer.pr_constr_env (Goal.V82.env s gl) s (EConstr.Unsafe.to_constr concl) ++
                 spc () ++ str ", " ++ int (List.length poss) ++
                 str" possibilities");
          match foundone with
@@ -793,7 +790,7 @@ module V85 = struct
                  let fk'' =
                    if not info.unique && List.is_empty gls' &&
                         not (needs_backtrack (Goal.V82.env s gl) s
-                                           info.is_evar (EConstr.Unsafe.to_constr (Goal.V82.concl s gl)))
+                                           info.is_evar (Goal.V82.concl s gl))
                    then fk
                    else fk'
                  in
@@ -984,7 +981,7 @@ module Search = struct
       NOT backtrack. *)
   let needs_backtrack env evd unique concl =
     if unique || is_Prop env evd concl then
-      occur_existential evd (EConstr.of_constr concl)
+      occur_existential evd concl
     else true
 
   let mark_unresolvables sigma goals =
@@ -1004,14 +1001,15 @@ module Search = struct
     let open Proofview.Notations in
     let env = Goal.env gl in
     let concl = Goal.concl gl in
+    let concl = EConstr.of_constr concl in
     let sigma = Goal.sigma gl in
     let s = Sigma.to_evar_map sigma in
-    let unique = not info.search_dep || is_unique env s (EConstr.of_constr concl) in
+    let unique = not info.search_dep || is_unique env s concl in
     let backtrack = needs_backtrack env s unique concl in
     if !typeclasses_debug > 0 then
       Feedback.msg_debug
         (pr_depth info.search_depth ++ str": looking for " ++
-           Printer.pr_constr_env (Goal.env gl) s concl ++
+           Printer.pr_constr_env (Goal.env gl) s (EConstr.Unsafe.to_constr concl) ++
            (if backtrack then str" with backtracking"
             else str" without backtracking"));
     let secvars = compute_secvars gl in
@@ -1126,7 +1124,7 @@ module Search = struct
          if !foundone == false && !typeclasses_debug > 0 then
            Feedback.msg_debug
              (pr_depth info.search_depth ++ str": no match for " ++
-                Printer.pr_constr_env (Goal.env gl) s concl ++
+                Printer.pr_constr_env (Goal.env gl) s (EConstr.Unsafe.to_constr concl) ++
                 spc () ++ str ", " ++ int (List.length poss) ++
                 str" possibilities");
          match e with
@@ -1523,8 +1521,9 @@ 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_unsafe_type_of gl (EConstr.of_constr c) in
-  let ce = mk_clenv_from gl (EConstr.of_constr c,EConstr.of_constr cty) in
+  let cty = pf_unsafe_type_of gl c in
+  let cty = EConstr.of_constr cty in
+  let ce = mk_clenv_from gl (c,cty) in
   let tac = { enter = fun gl -> (unify_e_resolve false flags).enter gl
     ((c,cty,Univ.ContextSet.empty),0,ce) } in
   Proofview.V82.of_tactic (Proofview.Goal.nf_enter tac) gl
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index 8db264ad95..027b7dcd76 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -30,7 +30,7 @@ val not_evar : constr -> unit Proofview.tactic
 
 val is_ground : constr -> tactic
 
-val autoapply : constr -> Hints.hint_db_name -> tactic
+val autoapply : EConstr.constr -> Hints.hint_db_name -> tactic
 
 module Search : sig
   val eauto_tac :
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 24e4de7506..5d42ed2d55 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -29,7 +29,6 @@ open Proofview.Notations
 let eauto_unif_flags = auto_flags_of_state full_transparent_state
 
 let e_give_exact ?(flags=eauto_unif_flags) c =
-  let c = EConstr.of_constr c in
   Proofview.Goal.enter { enter = begin fun gl ->
   let t1 = Tacmach.New.pf_unsafe_type_of gl c in
   let t1 = EConstr.of_constr t1 in
@@ -40,7 +39,7 @@ let e_give_exact ?(flags=eauto_unif_flags) c =
   else exact_check c
   end }
 
-let assumption id = e_give_exact (mkVar id)
+let assumption id = e_give_exact (EConstr.mkVar id)
 
 let e_assumption =
   Proofview.Goal.enter { enter = begin fun gl ->
@@ -49,7 +48,7 @@ let e_assumption =
 
 let registered_e_assumption =
   Proofview.Goal.enter { enter = begin fun gl ->
-  Tacticals.New.tclFIRST (List.map (fun id -> e_give_exact (mkVar id))
+  Tacticals.New.tclFIRST (List.map (fun id -> e_give_exact (EConstr.mkVar id))
               (Tacmach.New.pf_ids_of_hyps gl))
   end }
 
@@ -89,15 +88,14 @@ let rec prolog l n gl =
 
 let out_term = function
   | IsConstr (c, _) -> c
-  | IsGlobRef gr -> fst (Universes.fresh_global_instance (Global.env ()) gr)
+  | IsGlobRef gr -> EConstr.of_constr (fst (Universes.fresh_global_instance (Global.env ()) gr))
 
 let prolog_tac l n =
   Proofview.V82.tactic begin fun gl ->
   let map c =
     let (c, sigma) = Tactics.run_delayed (pf_env gl) (project gl) c in
-    let c = EConstr.Unsafe.to_constr c in
     let c = pf_apply (prepare_hint false (false,true)) gl (sigma, c) in
-    EConstr.of_constr (out_term c)
+    out_term c
   in
   let l = List.map map l in
   try (prolog l n gl)
@@ -116,7 +114,6 @@ let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l)
 let unify_e_resolve poly flags (c,clenv) =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
       let clenv', c = connect_hint_clenv poly c clenv gl in
-      let c = EConstr.of_constr c in
       Proofview.V82.tactic
 	(fun gls ->
 	 let clenv' = clenv_unique_resolver ~flags clenv' gls in
@@ -124,13 +121,13 @@ let unify_e_resolve poly flags (c,clenv) =
 		 (Proofview.V82.of_tactic (Tactics.Simple.eapply c)) gls)
     end }
 
-let hintmap_of secvars hdc concl =
+let hintmap_of sigma secvars hdc concl =
   match hdc with
   | None -> fun db -> Hint_db.map_none ~secvars db
   | Some hdc ->
-     if occur_existential Evd.empty (EConstr.of_constr concl) then (** FIXME *)
-       (fun db -> Hint_db.map_existential ~secvars hdc concl db)
-     else (fun db -> Hint_db.map_auto ~secvars hdc concl db)
+     if occur_existential sigma concl then
+       (fun db -> Hint_db.map_existential sigma ~secvars hdc concl db)
+     else (fun db -> Hint_db.map_auto sigma ~secvars hdc concl db)
    (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
 
 let e_exact poly flags (c,clenv) =
@@ -152,13 +149,13 @@ let rec e_trivial_fail_db db_list local_db =
   let tacl =
     registered_e_assumption ::
     (Tacticals.New.tclTHEN Tactics.intro next) ::
-    (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_nf_concl gl)))
+    (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (EConstr.of_constr (Tacmach.New.pf_nf_concl gl))))
   in
   Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl)
   end }
 
-and e_my_find_search db_list local_db secvars hdc concl =
-  let hint_of_db = hintmap_of secvars hdc concl in
+and e_my_find_search sigma db_list local_db secvars hdc concl =
+  let hint_of_db = hintmap_of sigma secvars hdc concl in
   let hintl =
       List.map_append (fun db ->
 	let flags = auto_flags_of_state (Hint_db.transparent_state db) in
@@ -188,13 +185,13 @@ and e_my_find_search db_list local_db secvars hdc concl =
 
 and e_trivial_resolve sigma db_list local_db secvars gl =
   let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in
-  try priority (e_my_find_search db_list local_db secvars hd gl)
+  try priority (e_my_find_search sigma db_list local_db secvars hd gl)
   with Not_found -> []
 
 let e_possible_resolve sigma db_list local_db secvars gl =
   let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in
   try List.map (fun (b, (tac, pp)) -> (tac, b, pp))
-               (e_my_find_search db_list local_db secvars hd gl)
+               (e_my_find_search sigma db_list local_db secvars hd gl)
   with Not_found -> []
 
 let find_first_goal gls =
@@ -265,7 +262,7 @@ module SearchProblem = struct
       let g = find_first_goal lg in
       let hyps = pf_ids_of_hyps g in
       let secvars = secvars_of_hyps (pf_hyps g) in
-      let map_assum id = (e_give_exact (mkVar id), (-1), lazy (str "exact" ++ spc () ++ pr_id id)) in
+      let map_assum id = (e_give_exact (EConstr.mkVar id), (-1), lazy (str "exact" ++ spc () ++ pr_id id)) in
       let assumption_tacs =
         let tacs = List.map map_assum hyps in
         let l = filter_tactics s.tacres tacs in
@@ -293,6 +290,7 @@ module SearchProblem = struct
       let rec_tacs =
 	let l =
           let concl = Reductionops.nf_evar (project g)(pf_concl g) in
+          let concl = EConstr.of_constr concl in
 	  filter_tactics s.tacres
                          (e_possible_resolve (project g) s.dblist (List.hd s.localdb) secvars concl)
 	in
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 1f69e4ab3c..defa34d9c6 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -15,7 +15,7 @@ val e_assumption : unit Proofview.tactic
 
 val registered_e_assumption : unit Proofview.tactic
 
-val e_give_exact : ?flags:Unification.unify_flags -> constr -> unit Proofview.tactic
+val e_give_exact : ?flags:Unification.unify_flags -> EConstr.constr -> unit Proofview.tactic
 
 val prolog_tac : delayed_open_constr list -> int -> unit Proofview.tactic
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index c31e863830..cd5fc79f5e 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -6,12 +6,16 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+module CVars = Vars
+
 open Pp
 open Util
 open CErrors
 open Names
-open Vars
 open Term
+open Evd
+open EConstr
+open Vars
 open Environ
 open Mod_subst
 open Globnames
@@ -21,7 +25,6 @@ open Libnames
 open Smartlocate
 open Misctypes
 open Tactypes
-open Evd
 open Termops
 open Inductiveops
 open Typing
@@ -46,22 +49,29 @@ type debug = Debug | Info | Off
 exception Bound
 
 let head_constr_bound sigma t =
-  let t = strip_outer_cast sigma (EConstr.of_constr t) in
-  let _,ccl = decompose_prod_assum t in
-  let hd,args = decompose_app ccl in
-  match kind_of_term hd with
-    | Const _ | Ind _ | Construct _ | Var _ -> hd
-    | Proj (p, _) -> mkConst (Projection.constant p)
-    | _ -> raise Bound
+  let t = strip_outer_cast sigma t in
+  let t = EConstr.of_constr t in
+  let _,ccl = decompose_prod_assum sigma t in
+  let hd,args = decompose_app sigma ccl in
+  match EConstr.kind sigma hd with
+  | Const (c, _) -> ConstRef c
+  | Ind (i, _) -> IndRef i
+  | Construct (c, _) -> ConstructRef c
+  | Var id -> VarRef id
+  | Proj (p, _) -> ConstRef (Projection.constant p)
+  | _ -> raise Bound
 
 let head_constr sigma c =
   try head_constr_bound sigma c with Bound -> error "Bound head variable."
 
 let decompose_app_bound sigma t =
-  let t = strip_outer_cast sigma (EConstr.of_constr t) in
-  let _,ccl = decompose_prod_assum t in
-  let hd,args = decompose_app_vect sigma (EConstr.of_constr ccl) in
-  match kind_of_term hd with
+  let t = strip_outer_cast sigma t in
+  let t = EConstr.of_constr t in
+  let _,ccl = decompose_prod_assum sigma t in
+  let hd,args = decompose_app_vect sigma ccl in
+  let hd = EConstr.of_constr hd in
+  let args = Array.map EConstr.of_constr args in
+  match EConstr.kind sigma hd with
     | Const (c,u) -> ConstRef c, args
     | Ind (i,u) -> IndRef i, args
     | Construct (c,u) -> ConstructRef c, args
@@ -245,6 +255,7 @@ let rebuild_dn st se =
   { se with sentry_bnet = dn' }
 
 let lookup_tacs concl st se =
+  let concl = EConstr.Unsafe.to_constr concl in
   let l'  = Bounded_net.lookup st se.sentry_bnet concl in
   let sl' = List.stable_sort pri_order_int l' in
   List.merge pri_order_int se.sentry_nopat sl'
@@ -256,10 +267,10 @@ let is_transparent_gr (ids, csts) = function
   | ConstRef cst -> Cpred.mem cst csts
   | IndRef _ | ConstructRef _ -> false
 
-let strip_params env c = 
-  match kind_of_term c with
+let strip_params env sigma c = 
+  match EConstr.kind sigma c with
   | App (f, args) -> 
-    (match kind_of_term f with
+    (match EConstr.kind sigma f with
     | Const (p,_) ->
       let cb = lookup_constant p env in
 	(match cb.Declarations.const_proj with
@@ -276,11 +287,9 @@ let strip_params env c =
 let instantiate_hint env sigma p =
   let mk_clenv (c, cty, ctx) =
     let sigma = Evd.merge_context_set univ_flexible sigma ctx in
-    let c = EConstr.of_constr c in
-    let cty = EConstr.of_constr cty in
     let cl = mk_clenv_from_env env sigma None (c,cty) in 
       {cl with templval = 
-	  { cl.templval with rebus = EConstr.of_constr (strip_params env (EConstr.Unsafe.to_constr cl.templval.rebus)) };
+	  { cl.templval with rebus = strip_params env sigma cl.templval.rebus };
 	env = empty_env}
   in
   let code = match p.code.obj with
@@ -445,11 +454,11 @@ val empty : ?name:hint_db_name -> transparent_state -> bool -> t
 val find : global_reference -> t -> search_entry
 val map_none : secvars:Id.Pred.t -> t -> full_hint list
 val map_all : secvars:Id.Pred.t -> global_reference -> t -> full_hint list
-val map_existential : secvars:Id.Pred.t ->
+val map_existential : evar_map -> secvars:Id.Pred.t ->
 		      (global_reference * constr array) -> constr -> t -> full_hint list
-val map_eauto : secvars:Id.Pred.t ->
+val map_eauto : evar_map -> secvars:Id.Pred.t ->
 		(global_reference * constr array) -> constr -> t -> full_hint list
-val map_auto : secvars:Id.Pred.t ->
+val map_auto : evar_map -> secvars:Id.Pred.t ->
 	       (global_reference * constr array) -> constr -> t -> full_hint list
 val add_one : env -> evar_map -> hint_entry -> t -> t
 val add_list : env -> evar_map -> hint_entry list -> t -> t
@@ -505,21 +514,21 @@ struct
       (** Warn about no longer typable hint? *)
       None
 
-  let match_mode m arg =
+  let match_mode sigma m arg =
     match m with
-    | ModeInput -> not (occur_existential Evd.empty (EConstr.of_constr arg)) (** FIXME *)
+    | ModeInput -> not (occur_existential sigma arg)
     | ModeNoHeadEvar ->
-       Evarutil.(try ignore(head_evar arg); false
+       Evarutil.(try ignore(head_evar sigma arg); false
                  with NoHeadEvar -> true)
     | ModeOutput -> true
                                
-  let matches_mode args mode =
+  let matches_mode sigma args mode =
     Array.length mode == Array.length args &&
-      Array.for_all2 match_mode mode args
+      Array.for_all2 (match_mode sigma) mode args
       
-  let matches_modes args modes =
+  let matches_modes sigma args modes =
     if List.is_empty modes then true
-    else List.exists (matches_mode args) modes
+    else List.exists (matches_mode sigma args) modes
 
   let merge_entry secvars db nopat pat =
     let h = List.sort pri_order_int (List.map snd db.hintdb_nopat) in
@@ -535,22 +544,22 @@ struct
     merge_entry secvars db se.sentry_nopat se.sentry_pat
 	
   (** Precondition: concl has no existentials *)
-  let map_auto ~secvars (k,args) concl db =
+  let map_auto sigma ~secvars (k,args) concl db =
     let se = find k db in
     let st = if db.use_dn then  (Some db.hintdb_state) else None in
     let pat = lookup_tacs concl st se in
     merge_entry secvars db [] pat
 
-  let map_existential ~secvars (k,args) concl db =
+  let map_existential sigma ~secvars (k,args) concl db =
     let se = find k db in
-      if matches_modes args se.sentry_mode then
+      if matches_modes sigma args se.sentry_mode then
         merge_entry secvars db se.sentry_nopat se.sentry_pat
       else merge_entry secvars db [] []
 
   (* [c] contains an existential *)
-  let map_eauto ~secvars (k,args) concl db =
+  let map_eauto sigma ~secvars (k,args) concl db =
     let se = find k db in
-      if matches_modes args se.sentry_mode then
+      if matches_modes sigma args se.sentry_mode then
         let st = if db.use_dn then Some db.hintdb_state else None in
         let pat = lookup_tacs concl st se in
         merge_entry secvars db [] pat
@@ -718,8 +727,8 @@ let _ = Summary.declare_summary "search"
 (*             Auxiliary functions to prepare AUTOHINT objects            *)
 (**************************************************************************)
 
-let rec nb_hyp c = match kind_of_term c with
-  | Prod(_,_,c2) -> if noccurn 1 c2 then 1+(nb_hyp c2) else nb_hyp c2
+let rec nb_hyp sigma c = match EConstr.kind sigma c with
+  | Prod(_,_,c2) -> if noccurn sigma 1 c2 then 1+(nb_hyp sigma c2) else nb_hyp sigma c2
   | _ -> 0
 
 (* adding and removing tactics in the search table *)
@@ -736,19 +745,20 @@ let secvars_of_idset s =
         Id.Pred.add id p
       else p) s Id.Pred.empty
 
-let secvars_of_constr env c =
-  secvars_of_idset (Environ.global_vars_set env c)
+let secvars_of_constr env sigma c =
+  secvars_of_idset (Termops.global_vars_set env sigma c)
 
 let secvars_of_global env gr =
   secvars_of_idset (vars_of_global_reference env gr)
 
 let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
-  let secvars = secvars_of_constr env c in
-  let cty = strip_outer_cast sigma (EConstr.of_constr cty) in
-    match kind_of_term cty with
+  let secvars = secvars_of_constr env sigma c in
+  let cty = strip_outer_cast sigma cty in
+  let cty = EConstr.of_constr cty in
+    match EConstr.kind sigma cty with
     | Prod _ -> failwith "make_exact_entry"
     | _ ->
-	let pat = Patternops.pattern_of_constr env sigma (EConstr.of_constr cty) in
+	let pat = Patternops.pattern_of_constr env sigma cty in
 	let hd =
 	  try head_pattern_bound pat
 	  with BoundPattern -> failwith "make_exact_entry"
@@ -763,21 +773,21 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (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 (EConstr.of_constr cty) else cty in
-    match kind_of_term cty with
+  let cty = if hnf then EConstr.of_constr (hnf_constr env sigma cty) else cty in
+    match EConstr.kind sigma cty with
     | Prod _ ->
         let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
-        let ce = mk_clenv_from_env env sigma' None (EConstr.of_constr c,EConstr.of_constr cty) in
+        let ce = mk_clenv_from_env env sigma' None (c,cty) in
 	let c' = clenv_type (* ~reduce:false *) ce in
 	let pat = Patternops.pattern_of_constr env ce.evd c' in
         let hd =
 	  try head_pattern_bound pat
           with BoundPattern -> failwith "make_apply_entry" in
         let nmiss = List.length (clenv_missing ce) in
-        let secvars = secvars_of_constr env c in
+        let secvars = secvars_of_constr env sigma c in
 	if Int.equal nmiss 0 then
 	  (Some hd,
-          { pri = (match pri with None -> nb_hyp cty | Some p -> p);
+          { pri = (match pri with None -> nb_hyp sigma' cty | Some p -> p);
 	    poly = poly;
             pat = Some pat;
 	    name = name;
@@ -787,10 +797,10 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
 	else begin
 	  if not eapply then failwith "make_apply_entry";
           if verbose then
-	    Feedback.msg_info (str "the hint: eapply " ++ pr_lconstr c ++
+	    Feedback.msg_info (str "the hint: eapply " ++ pr_lconstr (EConstr.Unsafe.to_constr c) ++
 	    str " will only be used by eauto");
           (Some hd,
-           { pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p);
+           { pri = (match pri with None -> nb_hyp sigma' cty + nmiss | Some p -> p);
 	     poly = poly;
              pat = Some pat;
 	     name = name;
@@ -808,7 +818,7 @@ let pr_hint_term env sigma ctx = function
   | IsGlobRef gr -> pr_global gr
   | IsConstr (c, ctx) ->
      let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
-     pr_constr_env env sigma c
+     pr_constr_env env sigma (EConstr.Unsafe.to_constr c)
 
 (** We need an object to record the side-effect of registering
   global universes associated with a hint. *)
@@ -834,7 +844,8 @@ let fresh_global_or_constr env sigma poly cr =
   let isgr, (c, ctx) =
     match cr with
     | IsGlobRef gr ->
-       true, Universes.fresh_global_instance env gr
+      let (c, ctx) = Universes.fresh_global_instance env gr in
+       true, (EConstr.of_constr c, ctx)
     | IsConstr (c, ctx) -> false, (c, ctx)
   in
     if poly then (c, ctx)
@@ -848,7 +859,8 @@ let fresh_global_or_constr env sigma poly cr =
 
 let make_resolves env sigma flags pri poly ?name cr =
   let c, ctx = fresh_global_or_constr env sigma poly cr in
-  let cty = Retyping.get_type_of env sigma (EConstr.of_constr c) in
+  let cty = Retyping.get_type_of env sigma c in
+  let cty = EConstr.of_constr cty in
   let try_apply f =
     try Some (f (c, cty, ctx)) with Failure _ -> None in
   let ents = List.map_filter try_apply
@@ -857,7 +869,7 @@ let make_resolves env sigma flags pri poly ?name cr =
   in
   if List.is_empty ents then
     user_err ~hdr:"Hint"
-      (pr_lconstr c ++ spc() ++
+      (pr_lconstr (EConstr.Unsafe.to_constr c) ++ spc() ++
         (if pi1 flags then str"cannot be used as a hint."
 	else str "can be used as a hint only for eauto."));
   ents
@@ -869,7 +881,7 @@ let make_resolve_hyp env sigma decl =
   try
     [make_apply_entry env sigma (true, true, false) None false
        ~name:(PathHints [VarRef hname])
-       (c, NamedDecl.get_type decl, Univ.ContextSet.empty)]
+       (c, EConstr.of_constr (NamedDecl.get_type decl), Univ.ContextSet.empty)]
   with
     | Failure _ -> []
     | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp")
@@ -899,6 +911,7 @@ let make_extern pri pat tacast =
      code = with_uid (Extern tacast) })  
 
 let make_mode ref m = 
+  let open Term in
   let ty = Global.type_of_global_unsafe ref in
   let ctx, t = decompose_prod ty in
   let n = List.length ctx in
@@ -912,15 +925,16 @@ 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 (EConstr.of_constr (unsafe_type_of env sigma (EConstr.of_constr c))) in
-  let hd = head_of_constr_reference sigma (EConstr.of_constr (head_constr sigma t)) in
-  let ce = mk_clenv_from_env env sigma None (EConstr.of_constr c,EConstr.of_constr t) in
+  let t = hnf_constr env sigma (EConstr.of_constr (unsafe_type_of env sigma c)) in
+  let t = EConstr.of_constr t in
+  let hd = head_constr sigma t in
+  let ce = mk_clenv_from_env env sigma None (c,t) in
   (Some hd, { pri=1;
 	      poly = poly;
               pat = Some (Patternops.pattern_of_constr env ce.evd (clenv_type ce));
 	      name = name;
               db = None;
-              secvars = secvars_of_constr env c;
+              secvars = secvars_of_constr env sigma c;
               code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) })
 
 
@@ -1014,14 +1028,16 @@ let cache_autohint (kn, obj) =
 let subst_autohint (subst, obj) =
   let subst_key gr =
     let (lab'', elab') = subst_global subst gr in
+    let elab' = EConstr.of_constr elab' in
     let gr' =
-      (try head_of_constr_reference Evd.empty (EConstr.of_constr (head_constr_bound Evd.empty (** FIXME *) elab'))
+      (try head_constr_bound Evd.empty elab'
        with Bound -> lab'')
     in if gr' == gr then gr else gr'
   in
   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 subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in
     let code' = match data.code.obj with
       | Res_pf (c,t,ctx) ->
           let c' = subst_mps subst c in
@@ -1191,31 +1207,33 @@ let prepare_hint check (poly,local) env init (sigma,c) =
      It is actually a bit stupid to generalize over evars since the first
      thing make_resolves will do is to re-instantiate the products *)
   let sigma, subst = Evd.nf_univ_variables sigma in
-  let c = Vars.subst_univs_constr subst (Evarutil.nf_evar sigma c) in
-  let c = drop_extra_implicit_args sigma (EConstr.of_constr c) in
-  let vars = ref (collect_vars sigma (EConstr.of_constr c)) in
+  let c = Evarutil.nf_evar sigma (EConstr.Unsafe.to_constr c) in
+  let c = CVars.subst_univs_constr subst c in
+  let c = EConstr.of_constr c in
+  let c = drop_extra_implicit_args sigma c in
+  let vars = ref (collect_vars sigma c) in
   let subst = ref [] in
-  let rec find_next_evar c = match kind_of_term c with
+  let rec find_next_evar c = match EConstr.kind sigma c with
     | Evar (evk,args as ev) ->
       (* We skip the test whether args is the identity or not *)
-      let t = Evarutil.nf_evar sigma (existential_type sigma ev) in
-      let t = List.fold_right (fun (e,id) c -> replace_term sigma (EConstr.of_constr e) (EConstr.of_constr id) (EConstr.of_constr c)) !subst t in
-      if not (closed0 c) then
+      let t = existential_type sigma ev in
+      let t = List.fold_right (fun (e,id) c -> EConstr.of_constr (replace_term sigma e id c)) !subst t in
+      if not (closed0 sigma c) then
 	error "Hints with holes dependent on a bound variable not supported.";
-      if occur_existential sigma (EConstr.of_constr t) then
+      if occur_existential sigma t then
 	(* Not clever enough to construct dependency graph of evars *)
 	error "Not clever enough to deal with evars dependent in other evars.";
       raise (Found (c,t))
-    | _ -> Constr.iter find_next_evar c in
+    | _ -> EConstr.iter sigma find_next_evar c in
   let rec iter c =
     try find_next_evar c; c
     with Found (evar,t) ->
       let id = next_ident_away_from default_prepare_hint_ident (fun id -> Id.Set.mem id !vars) in
       vars := Id.Set.add id !vars;
       subst := (evar,mkVar id)::!subst;
-      mkNamedLambda id t (iter (replace_term sigma (EConstr.of_constr evar) (EConstr.mkVar id) (EConstr.of_constr c))) in
+      mkNamedLambda id t (iter (EConstr.of_constr (replace_term sigma evar (mkVar id) c))) in
   let c' = iter c in
-    if check then Pretyping.check_evars (Global.env()) Evd.empty sigma (EConstr.of_constr c');
+    if check then Pretyping.check_evars (Global.env()) Evd.empty sigma c';
     let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
     if poly then IsConstr (c', diff)
     else if local then IsConstr (c', diff)
@@ -1228,6 +1246,7 @@ let interp_hints poly =
   let sigma = Evd.from_env env in
   let f poly c =
     let evd,c = Constrintern.interp_open_constr env sigma c in
+    let c = EConstr.of_constr c in
       prepare_hint true (poly,false) (Global.env()) Evd.empty (evd,c) in
   let fref r =
     let gr = global_with_alias r in
@@ -1293,7 +1312,7 @@ let add_hints local dbnames0 h =
 
 let expand_constructor_hints env sigma lems =
   List.map_append (fun (evd,lem) ->
-    match kind_of_term lem with
+    match EConstr.kind sigma lem with
     | Ind (ind,u) ->
 	List.init (nconstructors ind) 
 		  (fun i ->
@@ -1320,7 +1339,7 @@ let make_local_hint_db env sigma ts eapply lems =
   let map c =
     let sigma = Sigma.Unsafe.of_evar_map sigma in
     let Sigma (c, sigma, _) = c.delayed env sigma in
-    (Sigma.to_evar_map sigma, EConstr.Unsafe.to_constr c)
+    (Sigma.to_evar_map sigma, c)
   in
   let lems = List.map map lems in
   let sign = Environ.named_context env in
@@ -1348,7 +1367,7 @@ let make_db_list dbnames =
 (*                    Functions for printing the hints                    *)
 (**************************************************************************)
 
-let pr_hint_elt (c, _, _) = pr_constr c
+let pr_hint_elt (c, _, _) = pr_constr (EConstr.Unsafe.to_constr c)
 
 let pr_hint h = match h.obj with
   | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt c)
@@ -1402,9 +1421,9 @@ let pr_hint_term sigma cl =
     let valid_dbs =
       let fn = try
 	  let hdc = decompose_app_bound sigma cl in
-	    if occur_existential sigma (EConstr.of_constr cl) then
-	      Hint_db.map_existential ~secvars:Id.Pred.full hdc cl
-	    else Hint_db.map_auto ~secvars:Id.Pred.full hdc cl
+	    if occur_existential sigma cl then
+	      Hint_db.map_existential sigma ~secvars:Id.Pred.full hdc cl
+	    else Hint_db.map_auto sigma ~secvars:Id.Pred.full hdc cl
 	with Bound -> Hint_db.map_none ~secvars:Id.Pred.full
       in
       let fn db = List.map (fun x -> 0, x) (fn db) in
@@ -1425,7 +1444,7 @@ let pr_applicable_hint () =
   match glss.Evd.it with
   | [] -> CErrors.error "No focused goal."
   | g::_ ->
-    pr_hint_term glss.Evd.sigma (EConstr.Unsafe.to_constr (Goal.V82.concl glss.Evd.sigma g))
+    pr_hint_term glss.Evd.sigma (Goal.V82.concl glss.Evd.sigma g)
 
 let pp_hint_mode = function
   | ModeInput -> str"+"
diff --git a/tactics/hints.mli b/tactics/hints.mli
index c0eb2c3b86..344827e03e 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -10,6 +10,7 @@ open Pp
 open Util
 open Names
 open Term
+open EConstr
 open Environ
 open Globnames
 open Decl_kinds
@@ -99,16 +100,16 @@ module Hint_db :
 
     (** All hints associated to the reference, respecting modes if evars appear in the 
 	arguments, _not_ using the discrimination net. *)
-    val map_existential : secvars:Id.Pred.t ->
+    val map_existential : evar_map -> secvars:Id.Pred.t ->
       (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 : secvars:Id.Pred.t -> (global_reference * constr array) -> constr -> t -> full_hint list
+    val map_eauto : evar_map -> secvars:Id.Pred.t -> (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 : secvars:Id.Pred.t ->
+    val map_auto : evar_map -> secvars:Id.Pred.t ->
        (global_reference * constr array) -> constr -> t -> full_hint list
 
     val add_one : env -> evar_map -> hint_entry -> t -> t
@@ -170,7 +171,7 @@ val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit
 
 val prepare_hint : bool (* Check no remaining evars *) ->
   (bool * bool) (* polymorphic or monomorphic, local or global *) ->
-  env -> evar_map -> open_constr -> hint_term
+  env -> evar_map -> evar_map * constr -> hint_term
 
 (** [make_exact_entry pri (c, ctyp, ctx, secvars)].
    [c] is the term given as an exact proof to solve the goal;