Removing most nf_enter in tactics.

Now they are useless because all of the primitives are (should?) be
evar-insensitive.

3 files changed, 22 insertions, 10 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 5645850b2..f9ebc4233 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -129,11 +129,13 @@ let mk_clenv_from_env env sigma n (c,cty) =
     env = env }
 
 let mk_clenv_from_n gls n (c,cty) =
-  mk_clenv_from_env (pf_env gls) gls.sigma n (c, cty)
+  let env = Proofview.Goal.env gls in
+  let sigma = Tacmach.New.project gls in
+  mk_clenv_from_env env sigma n (c, cty)
 
 let mk_clenv_from gls = mk_clenv_from_n gls None
 
-let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
+let mk_clenv_type_of gls t = mk_clenv_from gls (t,Tacmach.New.pf_unsafe_type_of gls t)
 
 (******************************************************************)
 
@@ -263,8 +265,7 @@ let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv =
 let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
   { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
 
-let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
-  let concl = Goal.V82.concl clenv.evd (sig_it gl) in
+let clenv_unique_resolver_gen ?(flags=default_unify_flags ()) clenv concl =
   if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd clenv.templtyp.rebus))) then
     clenv_unify CUMUL ~flags (clenv_type clenv) concl
       (clenv_unify_meta_types ~flags clenv)
@@ -272,6 +273,14 @@ let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
     clenv_unify CUMUL ~flags
       (meta_reducible_instance clenv.evd clenv.templtyp) concl clenv
 
+let old_clenv_unique_resolver ?flags clenv gl =
+  let concl = Goal.V82.concl clenv.evd (sig_it gl) in
+  clenv_unique_resolver_gen ?flags clenv concl
+
+let clenv_unique_resolver ?flags clenv gl =
+  let concl = Proofview.Goal.concl gl in
+  clenv_unique_resolver_gen ?flags clenv concl
+
 let adjust_meta_source evd mv = function
   | loc,Evar_kinds.VarInstance id ->
     let rec match_name c l =
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index f7ff4bed3..4bcd50591 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -41,10 +41,10 @@ val clenv_nf_meta   : clausenv -> EConstr.constr -> EConstr.constr
 (** type of a meta in clenv context *)
 val clenv_meta_type : clausenv -> metavariable -> types
 
-val mk_clenv_from : Goal.goal sigma -> EConstr.constr * EConstr.types -> clausenv
+val mk_clenv_from : ('a, 'r) Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv
 val mk_clenv_from_n :
-  Goal.goal sigma -> int option -> EConstr.constr * EConstr.types -> clausenv
-val mk_clenv_type_of : Goal.goal sigma -> EConstr.constr -> clausenv
+  ('a, 'r) Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv
+val mk_clenv_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> clausenv
 val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv
 
 (** Refresh the universes in a clenv *)
@@ -62,9 +62,12 @@ val clenv_unify :
   ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv
 
 (** unifies the concl of the goal with the type of the clenv *)
-val clenv_unique_resolver :
+val old_clenv_unique_resolver :
   ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
 
+val clenv_unique_resolver :
+  ?flags:unify_flags -> clausenv -> ('a, 'r) Proofview.Goal.t -> clausenv
+
 val clenv_dependent : clausenv -> metavariable list
 
 val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 32c887ff5..0722ea047 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -105,8 +105,8 @@ let dft = default_unify_flags
 
 let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv =
   Proofview.Goal.enter { enter = begin fun gl ->
-    let clenv gl = clenv_unique_resolver ~flags clenv gl in
-    clenv_refine with_evars ~with_classes (Tacmach.New.of_old clenv (Proofview.Goal.assume gl))
+    let clenv = clenv_unique_resolver ~flags clenv gl in
+    clenv_refine with_evars ~with_classes clenv
   end }
 
 (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en