Evar-normalizing functions now act on EConstrs.

8 files changed, 10 insertions, 15 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index b548f8b92..17a488ddb 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -321,7 +321,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
       ( Proofview.Goal.enter { enter = begin fun gl ->
           let sigma = Tacmach.New.project gl in
           let env = Proofview.Goal.env gl in
-          let nf c = Evarutil.nf_evar sigma c in
+          let nf c = EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr c)) in
           let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in
           let hyp = Context.Named.Declaration.map_constr nf decl in
 	  let hintl = make_resolve_hyp env sigma hyp
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index fa2c21ac3..a4b6cb53b 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -521,8 +521,7 @@ let evars_to_goals p evm =
 (** Making local hints  *)
 let make_resolve_hyp env sigma st flags only_classes pri decl =
   let id = NamedDecl.get_id decl in
-  let cty = Evarutil.nf_evar sigma (NamedDecl.get_type decl) in
-  let cty = EConstr.of_constr cty in
+  let cty = Evarutil.nf_evar sigma (EConstr.of_constr (NamedDecl.get_type decl)) in
   let rec iscl env ty =
     let ctx, ar = decompose_prod_assum sigma ty in
       match EConstr.kind sigma (fst (decompose_app sigma ar)) with
@@ -1476,8 +1475,7 @@ let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique =
   in
   let evd = sig_sig gls' in
   let t' = mkEvar (ev, Array.of_list subst) in
-  let term = Evarutil.nf_evar evd (EConstr.Unsafe.to_constr t') in
-  let term = EConstr.of_constr term in
+  let term = Evarutil.nf_evar evd t' in
     evd, term
 
 let _ =
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index a3a448aad..7173fb4fd 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -66,8 +66,7 @@ let contradiction_context =
       | [] ->  Tacticals.New.tclZEROMSG (Pp.str"No such contradiction")
       | d :: rest ->
           let id = NamedDecl.get_id d in
-          let typ = nf_evar sigma (NamedDecl.get_type d) in
-          let typ = EConstr.of_constr typ in
+          let typ = nf_evar sigma (EConstr.of_constr (NamedDecl.get_type d)) in
 	  let typ = whd_all env sigma typ in
 	  if is_empty_type sigma typ then
 	    simplest_elim (mkVar id)
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 01f21910c..7453fff5c 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -289,8 +289,7 @@ module SearchProblem = struct
       in
       let rec_tacs =
 	let l =
-          let concl = Reductionops.nf_evar (project g) (EConstr.Unsafe.to_constr (pf_concl g)) in
-          let concl = EConstr.of_constr concl in
+          let concl = Reductionops.nf_evar (project g) (pf_concl g) in
 	  filter_tactics s.tacres
                          (e_possible_resolve (project g) s.dblist (List.hd s.localdb) secvars concl)
 	in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index c80cf4416..072da995d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1212,7 +1212,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
 	    error "Cannot solve a unification problem."
   in
   let scf = sigrec_clausal_form siglen ty in
-    !evdref, EConstr.of_constr (Evarutil.nf_evar !evdref (EConstr.Unsafe.to_constr scf))
+    !evdref, Evarutil.nf_evar !evdref scf
 
 (* The problem is to build a destructor (a generalization of the
    predecessor) which, when applied to a term made of constructors
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 851e9f01f..ef97b0b33 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1200,7 +1200,8 @@ 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 = Evarutil.nf_evar sigma (EConstr.Unsafe.to_constr c) in
+  let c = Evarutil.nf_evar sigma c in
+  let c = EConstr.Unsafe.to_constr c in
   let c = CVars.subst_univs_constr subst c in
   let c = EConstr.of_constr c in
   let c = drop_extra_implicit_args sigma c in
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 3199623e7..a05b4fbf3 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -208,14 +208,12 @@ let inversion_scheme env sigma t sort dep_option inv_op =
     user_err ~hdr:"lemma_inversion"
     (str"Computed inversion goal was not closed in initial signature.");
   *)
-  let invGoal = EConstr.Unsafe.to_constr invGoal in
   let pf = Proof.start (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
   let pf =
     fst (Proof.run_tactic env (
       tclTHEN intro (onLastHypId inv_op)) pf)
   in
   let pfterm = List.hd (Proof.partial_proof pf) in
-  let pfterm = EConstr.of_constr pfterm in
   let global_named_context = Global.named_context_val () in
   let ownSign = ref begin
     fold_named_context
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 10582288c..0ecccd5c0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2945,7 +2945,6 @@ let quantify lconstr =
 (* Modifying/Adding an hypothesis  *)
 
 let specialize (c,lbind) ipat =
-  let nf_evar sigma c = EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr c)) in
   Proofview.Goal.enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
@@ -3825,7 +3824,7 @@ let specialize_eqs id gl =
   let acc' = it_mkLambda_or_LetIn acc ctx'' in
   let ty' = Tacred.whd_simpl env !evars ty'
   and acc' = Tacred.whd_simpl env !evars acc' in
-  let ty' = EConstr.of_constr (Evarutil.nf_evar !evars (EConstr.Unsafe.to_constr ty')) in
+  let ty' = Evarutil.nf_evar !evars ty' in
     if worked then
       tclTHENFIRST (Tacmach.internal_cut true id ty')
 	(Proofview.V82.of_tactic (exact_no_check ((* refresh_universes_strict *) acc'))) gl
@@ -4951,6 +4950,7 @@ let abstract_subproof id gk tac =
     let ctx = Evd.universe_context_set evd in
       evd, ctx, nf concl
   in
+  let concl = EConstr.of_constr concl in
   let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in
   let ectx = Evd.evar_universe_context evd in
   let (const, safe, ectx) =