Ltac cleanup: no more constr_of_global calls

4 files changed, 28 insertions, 25 deletions

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index d68139a4b..2f2a5cdb0 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -306,7 +306,8 @@ let project_hint pri l2r r =
     | _ -> assert false in
   let p =
     if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in
-  let p = EConstr.of_constr @@ Universes.constr_of_global p in
+  let sigma, p = Evd.fresh_global env sigma p in
+  let p = EConstr.of_constr p in
   let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in
   let c = it_mkLambda_or_LetIn
     (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
@@ -735,7 +736,6 @@ let rewrite_except h =
 
 let refl_equal = 
   let coq_base_constant s =
-    Universes.constr_of_global @@
     Coqlib.gen_reference_in_modules "RecursiveDefinition"
       (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s in
   function () -> (coq_base_constant "eq_refl")
@@ -747,8 +747,9 @@ let refl_equal =
 let  mkCaseEq a  : unit Proofview.tactic =
   Proofview.Goal.enter { enter = begin fun gl ->
     let type_of_a = Tacmach.New.pf_unsafe_type_of gl a in
-       Tacticals.New.tclTHENLIST
-         [Tactics.generalize [(mkApp(EConstr.of_constr (delayed_force refl_equal), [| type_of_a; a|]))];
+    Tacticals.New.pf_constr_of_global (delayed_force refl_equal) >>= fun req ->
+    Tacticals.New.tclTHENLIST
+         [Tactics.generalize [(mkApp(req, [| type_of_a; a|]))];
           Proofview.Goal.enter { enter = begin fun gl ->
             let concl = Proofview.Goal.concl gl in
             let env = Proofview.Goal.env gl in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 966b11d0e..dadcfb9f2 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -751,17 +751,23 @@ let default_flags = { under_lambdas = true; on_morphisms = true; }
 
 let get_opt_rew_rel = function RewPrf (rel, prf) -> Some rel | _ -> None
 
-let make_eq () =
-(*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ()))
-let make_eq_refl () =
-(*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq_refl ()))
+let new_global (evars, cstrs) gr = 
+  let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map evars) gr
+  in (Sigma.to_evar_map sigma, cstrs), c
 
-let get_rew_prf r = match r.rew_prf with
-  | RewPrf (rel, prf) -> rel, prf 
+let make_eq sigma =
+  new_global sigma (Coqlib.build_coq_eq ())
+let make_eq_refl sigma =
+  new_global sigma (Coqlib.build_coq_eq_refl ())
+
+let get_rew_prf evars r = match r.rew_prf with
+  | RewPrf (rel, prf) -> evars, (rel, prf)
   | RewCast c ->
-    let rel = mkApp (make_eq (), [| r.rew_car |]) in
-      rel, mkCast (mkApp (make_eq_refl (), [| r.rew_car; r.rew_from |]),
-		   c, mkApp (rel, [| r.rew_from; r.rew_to |]))
+    let evars, eq = make_eq evars in
+    let evars, eq_refl = make_eq_refl evars in
+    let rel = mkApp (eq, [| r.rew_car |]) in
+    evars, (rel, mkCast (mkApp (eq_refl, [| r.rew_car; r.rew_from |]),
+		         c, mkApp (rel, [| r.rew_from; r.rew_to |])))
 
 let poly_subrelation sort = 
   if sort then PropGlobal.subrelation else TypeGlobal.subrelation
@@ -827,7 +833,8 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
 		      env evars carrier relation x in
 		    [ proof ; x ; x ] @ acc, subst, evars, sigargs, x :: typeargs'
 	      | Some r ->
-		  [ snd (get_rew_prf r); r.rew_to; x ] @ acc, subst, evars, 
+                 let evars, proof = get_rew_prf evars r in
+		 [ snd proof; r.rew_to; x ] @ acc, subst, evars, 
 	      sigargs, r.rew_to :: typeargs')
 	  | None ->
 	      if not (Option.is_empty y) then 
@@ -847,7 +854,8 @@ let apply_constraint env avoid car rel prf cstr res =
   | Some r -> resolve_subrelation env avoid car rel (fst cstr) prf r res
 
 let coerce env avoid cstr res = 
-  let rel, prf = get_rew_prf res in
+  let evars, (rel, prf) = get_rew_prf res.rew_evars res in
+  let res = { res with rew_evars = evars } in
     apply_constraint env avoid res.rew_car rel prf cstr res
 
 let apply_rule unify loccs : int pure_strategy =
@@ -868,8 +876,7 @@ let apply_rule unify loccs : int pure_strategy =
 	    else if Termops.eq_constr (fst rew.rew_evars) 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 unfresh rew.rew_car rel prf cstr res) in
+	      let res = Success (coerce env unfresh cstr res) in
               (occ, res)
     }
 
@@ -1231,9 +1238,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 	in 
 	let res = 
 	  match res with
-	  | Success r ->  
-	    let rel, prf = get_rew_prf r in
-	      Success (apply_constraint env unfresh r.rew_car rel prf (prop,cstr) r)
+	  | Success r -> Success (coerce env unfresh (prop,cstr) r)
 	  | Fail | Identity -> res
 	in state, res
       | _ -> state, Fail
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 4390ff08b..8cbe9c690 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -14,7 +14,6 @@ open Stdarg
 open Tacarg
 open Misctypes
 open Globnames
-open Term
 open Genredexpr
 open Patternops
 
@@ -91,7 +90,7 @@ open Printer
 let subst_global_reference subst =
  let subst_global ref =
   let ref',t' = subst_global subst ref in
-   if not (eq_constr (Universes.constr_of_global ref') t') then
+   if not (is_global ref' t') then
     Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++
           str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++
           pr_global ref') ;
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 4ec111e01..d8e21d81d 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -220,9 +220,7 @@ let apply_nnpp _ ist =
   Proofview.tclBIND
     (Proofview.tclUNIT ())
     begin fun () -> try
-      let nnpp = Universes.constr_of_global (Nametab.global_of_path coq_nnpp_path) in
-      let nnpp = EConstr.of_constr nnpp in
-      apply nnpp
+      Tacticals.New.pf_constr_of_global (Nametab.global_of_path coq_nnpp_path) >>= apply
     with Not_found -> tclFAIL 0 (Pp.mt ())
     end