tactics cleanup: remove constr_of_global calls

8 files changed, 79 insertions, 56 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index c0485e4e7..5a05150d4 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -782,6 +782,9 @@ let fresh_global ?loc ?rigid ?names env sigma reference =
     Sigma.fresh_global ?loc ?rigid ?names env sigma reference in
   Sigma.Sigma (of_constr t,sigma,p)
 
+let is_global sigma gr c =
+  Globnames.is_global gr (to_constr sigma c)
+
 module Unsafe =
 struct
 let to_sorts = ESorts.unsafe_to_sorts
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 9d705b4d5..9f45187cf 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -261,6 +261,8 @@ val fresh_global :
   ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
   'r Sigma.t -> Globnames.global_reference -> (t, 'r) Sigma.sigma
 
+val is_global : Evd.evar_map -> Globnames.global_reference -> t -> bool
+
 (** {5 Extra} *)
 
 val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, types) Context.Named.Declaration.pt
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index fe44559ed..5e7090ded 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -19,10 +19,9 @@ module NamedDecl = Context.Named.Declaration
 
 (* Absurd *)
 
-let mk_absurd_proof t =
-  let build_coq_not () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_not ()) in
+let mk_absurd_proof coq_not t =
   let id = Namegen.default_dependent_ident in
-  mkLambda (Names.Name id,mkApp(build_coq_not (),[|t|]),
+  mkLambda (Names.Name id,mkApp(coq_not,[|t|]),
     mkLambda (Names.Name id,t,mkApp (mkRel 2,[|mkRel 1|])))
 
 let absurd c =
@@ -34,9 +33,11 @@ let absurd c =
     let sigma, j = Coercion.inh_coerce_to_sort env sigma j in
     let t = j.Environ.utj_val in
     let tac =
+    Tacticals.New.pf_constr_of_global (build_coq_not ()) >>= fun coqnot ->
+    Tacticals.New.pf_constr_of_global (build_coq_False ()) >>= fun coqfalse ->
     Tacticals.New.tclTHENLIST [
-      elim_type (EConstr.of_constr (Universes.constr_of_global @@ build_coq_False ()));
-      Simple.apply (mk_absurd_proof t)
+      elim_type coqfalse;
+      Simple.apply (mk_absurd_proof coqnot t)
     ] in
     Sigma.Unsafe.of_pair (tac, sigma)
   end }
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index bda25d7f0..48ce52f09 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -104,14 +104,9 @@ let solveNoteqBranch side =
 
 (* Constructs the type {c1=c2}+{~c1=c2} *)
 
-let make_eq () =
-(*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ()))
-let build_coq_not () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_not ())
-let build_coq_sumbool () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_sumbool ())
-
-let mkDecideEqGoal eqonleft op rectype c1 c2 =
-  let equality    = mkApp(make_eq(), [|rectype; c1; c2|]) in
-  let disequality = mkApp(build_coq_not (), [|equality|]) in
+let mkDecideEqGoal eqonleft (op,eq,neg) rectype c1 c2 =
+  let equality    = mkApp(eq, [|rectype; c1; c2|]) in
+  let disequality = mkApp(neg, [|equality|]) in
   if eqonleft then mkApp(op, [|equality; disequality |])
   else mkApp(op, [|disequality; equality |])
 
@@ -121,13 +116,13 @@ let mkDecideEqGoal eqonleft op rectype c1 c2 =
 let idx = Id.of_string "x"
 let idy = Id.of_string "y"
 
-let mkGenDecideEqGoal rectype g =
+let mkGenDecideEqGoal rectype ops g =
   let hypnames = pf_ids_of_hyps g in
   let xname    = next_ident_away idx hypnames
   and yname    = next_ident_away idy hypnames in
   (mkNamedProd xname rectype
      (mkNamedProd yname rectype
-        (mkDecideEqGoal true (build_coq_sumbool ())
+        (mkDecideEqGoal true ops
           rectype (mkVar xname) (mkVar yname))))
 
 let rec rewrite_and_clear hyps = match hyps with
@@ -256,9 +251,9 @@ let decideGralEquality =
 
 let decideEqualityGoal = tclTHEN intros decideGralEquality
 
-let decideEquality rectype =
+let decideEquality rectype ops =
   Proofview.Goal.enter { enter = begin fun gl ->
-  let decide = mkGenDecideEqGoal rectype gl in
+  let decide = mkGenDecideEqGoal rectype ops gl in
   (tclTHENS (cut decide) [default_auto;decideEqualityGoal])
   end }
 
@@ -266,11 +261,15 @@ let decideEquality rectype =
 (* The tactic Compare *)
 
 let compare c1 c2 =
+  pf_constr_of_global (build_coq_sumbool ()) >>= fun opc ->
+  pf_constr_of_global (Coqlib.build_coq_eq ()) >>= fun eqc ->
+  pf_constr_of_global (build_coq_not ()) >>= fun notc ->
   Proofview.Goal.enter { enter = begin fun gl ->
   let rectype = pf_unsafe_type_of gl c1 in
-  let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in
+  let ops = (opc,eqc,notc) in
+  let decide = mkDecideEqGoal true ops rectype c1 c2 in
   (tclTHENS (cut decide)
             [(tclTHEN  intro
              (tclTHEN (onLastHyp simplest_case) clear_last));
-             decideEquality rectype])
+             decideEquality rectype ops])
   end }
diff --git a/tactics/equality.ml b/tactics/equality.ml
index b48d60a4f..268daf6b6 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1332,8 +1332,6 @@ let inject_if_homogenous_dependent_pair ty =
     let sigma = Tacmach.New.project gl in
     let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in
     (* fetch the informations of the  pair *)
-    let ceq = Universes.constr_of_global Coqlib.glob_eq in
-    let ceq = EConstr.of_constr ceq in
     let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ in
     let existTconstr () = (Coqlib.build_sigma_type()).Coqlib.intro in
     (* check whether the equality deals with dep pairs or not *)
@@ -1352,16 +1350,18 @@ let inject_if_homogenous_dependent_pair ty =
       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_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
-    let inj2 = EConstr.of_constr @@ Universes.constr_of_global @@
-      Coqlib.coq_reference "inj_pair2_eq_dec is missing" ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
+    let inj2 = Coqlib.coq_reference "inj_pair2_eq_dec is missing" ["Logic";"Eqdep_dec"]
+                                    "inj_pair2_eq_dec" in
     let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in
     (* cut with the good equality and prove the requested goal *)
     tclTHENLIST
       [Proofview.tclEFFECTS eff;
        intro;
        onLastHyp (fun hyp ->
+        Tacticals.New.pf_constr_of_global Coqlib.glob_eq >>= fun ceq ->
         tclTHENS (cut (mkApp (ceq,new_eq_args)))
           [clear [destVar sigma hyp];
+           Tacticals.New.pf_constr_of_global inj2 >>= fun inj2 ->
            Proofview.V82.tactic (Tacmach.refine
              (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|])))
           ])]
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index fd5eabe64..0d974be8b 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -544,7 +544,7 @@ let match_eqdec sigma t =
         false,op_or,matches sigma (Lazy.force coq_eqdec_rev_pattern) t in
   match Id.Map.bindings subst with
   | [(_,typ);(_,c1);(_,c2)] ->
-      eqonleft, EConstr.of_constr (Universes.constr_of_global (Lazy.force op)), c1, c2, typ
+      eqonleft, Lazy.force op, c1, c2, typ
   | _ -> anomaly (Pp.str "Unexpected pattern")
 
 (* Patterns "~ ?" and "? -> False" *)
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 82a3d47b5..9110830aa 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -142,7 +142,7 @@ val is_matching_sigma : evar_map -> constr -> bool
 
 (** Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns
    [t,u,T] and a boolean telling if equality is on the left side *)
-val match_eqdec : evar_map -> constr -> bool * constr * constr * constr * constr
+val match_eqdec : evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr
 
 (** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *)
 val dest_nf_eq : ('a, 'r) Proofview.Goal.t -> constr -> (constr * constr * constr)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7e8cb4e63..3efaf0cc6 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3519,27 +3519,32 @@ let error_ind_scheme s =
   let s = if not (String.is_empty s) then s^" " else s in
   user_err ~hdr:"Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.")
 
-let glob c = EConstr.of_constr (Universes.constr_of_global c)
+let glob sigma gr =
+  let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr
+  in Sigma.to_evar_map sigma, c
 
-let coq_eq      = lazy (glob (Coqlib.build_coq_eq ()))
-let coq_eq_refl = lazy (glob (Coqlib.build_coq_eq_refl ()))
+let coq_eq sigma       = glob sigma (Coqlib.build_coq_eq ())
+let coq_eq_refl sigma  = glob sigma (Coqlib.build_coq_eq_refl ())
 
-let coq_heq      = lazy (EConstr.of_constr @@ Universes.constr_of_global (Coqlib.coq_reference"mkHEq" ["Logic";"JMeq"] "JMeq"))
-let coq_heq_refl = lazy (EConstr.of_constr @@ Universes.constr_of_global (Coqlib.coq_reference "mkHEq" ["Logic";"JMeq"] "JMeq_refl"))
+let coq_heq_ref        = lazy (Coqlib.coq_reference"mkHEq" ["Logic";"JMeq"] "JMeq")
+let coq_heq sigma      = glob sigma (Lazy.force coq_heq_ref)
+let coq_heq_refl sigma = glob sigma (Coqlib.coq_reference "mkHEq" ["Logic";"JMeq"] "JMeq_refl")
 
-let mkEq t x y =
-  mkApp (Lazy.force coq_eq, [| t; x; y |])
+let mkEq sigma t x y =
+  let sigma, eq = coq_eq sigma in
+  sigma, mkApp (eq, [| t; x; y |])
 
-let mkRefl t x =
-  mkApp (Lazy.force coq_eq_refl, [| t; x |])
+let mkRefl sigma t x =
+  let sigma, refl = coq_eq_refl sigma in
+  sigma, mkApp (refl, [| t; x |])
 
-let mkHEq t x u y =
-  mkApp (Lazy.force coq_heq,
-	[| t; x; u; y |])
+let mkHEq sigma t x u y =
+  let sigma, c = coq_heq sigma in
+  sigma, mkApp (c,[| t; x; u; y |])
 
-let mkHRefl t x =
-  mkApp (Lazy.force coq_heq_refl,
-	[| t; x |])
+let mkHRefl sigma t x =
+  let sigma, c = coq_heq_refl sigma in
+  sigma, mkApp (c, [| t; x |])
 
 let lift_togethern n l =
   let l', _ =
@@ -3577,23 +3582,30 @@ let decompose_indapp sigma f args =
 	mkApp (f, pars), args
   | _ -> f, args
 
-let mk_term_eq env sigma ty t ty' t' =
+let mk_term_eq homogeneous env sigma ty t ty' t' =
   let sigma = Sigma.to_evar_map sigma in
-  if Reductionops.is_conv env sigma ty ty' then
-    mkEq ty t t', mkRefl ty' t'
+  if homogeneous then
+    let sigma, eq = mkEq sigma ty t t' in
+    let sigma, refl = mkRefl sigma ty' t' in
+    Sigma.Unsafe.of_evar_map sigma, (eq, refl)
   else
-    mkHEq ty t ty' t', mkHRefl ty' t'
+    let sigma, heq = mkHEq sigma ty t ty' t' in
+    let sigma, hrefl = mkHRefl sigma ty' t' in
+    Sigma.Unsafe.of_evar_map sigma, (heq, hrefl)
 
 let make_abstract_generalize env id typ concl dep ctx body c eqs args refls =
   let open Context.Rel.Declaration in
   Refine.refine { run = begin fun sigma ->
   let eqslen = List.length eqs in
     (* Abstract by the "generalized" hypothesis equality proof if necessary. *)
-  let abshypeq, abshypt =
+  let sigma, abshypeq, abshypt =
     if dep then
-      let eq, refl = mk_term_eq (push_rel_context ctx env) sigma (lift 1 c) (mkRel 1) typ (mkVar id) in
-	mkProd (Anonymous, eq, lift 1 concl), [| refl |]
-    else concl, [||]
+      let ty = lift 1 c in
+      let homogeneous = Reductionops.is_conv env (Sigma.to_evar_map sigma) ty typ in
+      let sigma, (eq, refl) =
+        mk_term_eq homogeneous (push_rel_context ctx env) sigma ty (mkRel 1) typ (mkVar id) in
+      sigma, mkProd (Anonymous, eq, lift 1 concl), [| refl |]
+    else sigma, concl, [||]
   in
     (* Abstract by equalities *)
   let eqs = lift_togethern 1 eqs in (* lift together and past genarg *)
@@ -3699,9 +3711,13 @@ let abstract_args gl generalize_vars dep id defined f args =
 	  let liftarg = lift (List.length ctx) arg in
 	  let eq, refl =
 	    if leq then
-	      mkEq (lift 1 ty) (mkRel 1) liftarg, mkRefl (lift (-lenctx) ty) arg
+	      let sigma', eq = mkEq !sigma (lift 1 ty) (mkRel 1) liftarg in
+              let sigma', refl = mkRefl sigma' (lift (-lenctx) ty) arg in
+              sigma := sigma'; eq, refl
 	    else
-	      mkHEq (lift 1 ty) (mkRel 1) liftargty liftarg, mkHRefl argty arg
+	      let sigma', eq = mkHEq !sigma (lift 1 ty) (mkRel 1) liftargty liftarg in
+              let sigma', refl = mkHRefl sigma' argty arg in
+              sigma := sigma'; eq, refl
 	  in
 	  let eqs = eq :: lift_list eqs in
 	  let refls = refl :: refls in
@@ -3801,17 +3817,19 @@ let specialize_eqs id gl =
     match EConstr.kind !evars ty with
     | Prod (na, t, b) ->
 	(match EConstr.kind !evars t with
-	| App (eq, [| eqty; x; y |]) when EConstr.eq_constr !evars (Lazy.force coq_eq) eq ->
+	| App (eq, [| eqty; x; y |]) when EConstr.is_global !evars (Lazy.force coq_eq_ref) eq ->
 	    let c = if noccur_between !evars 1 (List.length ctx) x then y else x in
-	    let pt = mkApp (Lazy.force coq_eq, [| eqty; c; c |]) in
-	    let p = mkApp (Lazy.force coq_eq_refl, [| eqty; c |]) in
+	    let pt = mkApp (eq, [| eqty; c; c |]) in
+            let ind = destInd !evars eq in
+	    let p = mkApp (mkConstructUi (ind,0), [| eqty; c |]) in
 	      if unif (push_rel_context ctx env) evars pt t then
 		aux true ctx (mkApp (acc, [| p |])) (subst1 p b)
 	      else acc, in_eqs, ctx, ty
-	| App (heq, [| eqty; x; eqty'; y |]) when EConstr.eq_constr !evars heq (Lazy.force coq_heq) ->
+	| App (heq, [| eqty; x; eqty'; y |]) when EConstr.is_global !evars (Lazy.force coq_heq_ref) heq ->
 	    let eqt, c = if noccur_between !evars 1 (List.length ctx) x then eqty', y else eqty, x in
-	    let pt = mkApp (Lazy.force coq_heq, [| eqt; c; eqt; c |]) in
-	    let p = mkApp (Lazy.force coq_heq_refl, [| eqt; c |]) in
+	    let pt = mkApp (heq, [| eqt; c; eqt; c |]) in
+            let ind = destInd !evars heq in
+	    let p = mkApp (mkConstructUi (ind,0), [| eqt; c |]) in
 	      if unif (push_rel_context ctx env) evars pt t then
 		aux true ctx (mkApp (acc, [| p |])) (subst1 p b)
 	      else acc, in_eqs, ctx, ty