Merge PR#696: Trunk+cleanup constr of global

7 files changed, 96 insertions, 72 deletions

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 e6278943d..268daf6b6 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -874,7 +874,7 @@ let descend_then env sigma head dirn =
   let dirn_env = Environ.push_rel_context cstr.(dirn-1).cs_args env in
   (dirn_nlams,
    dirn_env,
-   (fun dirnval (dfltval,resty) ->
+   (fun sigma dirnval (dfltval,resty) ->
       let deparsign = make_arity_signature env sigma true indf in
       let p =
 	it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in
@@ -887,7 +887,7 @@ let descend_then env sigma head dirn =
         List.map build_branch
           (List.interval 1 (Array.length mip.mind_consnames)) in
       let ci = make_case_info env ind RegularStyle in
-      Inductiveops.make_case_or_project env sigma indf ci p head (Array.of_list brl)))
+      sigma, Inductiveops.make_case_or_project env sigma indf ci p head (Array.of_list brl)))
 
 (* Now we need to construct the discriminator, given a discriminable
    position.  This boils down to:
@@ -932,23 +932,28 @@ let build_selector env sigma dirn c ind special default =
   let brl =
     List.map build_branch(List.interval 1 (Array.length mip.mind_consnames)) in
   let ci = make_case_info env ind RegularStyle in
-  mkCase (ci, p, c, Array.of_list brl)
+  sigma, mkCase (ci, p, c, Array.of_list brl)
 
-let build_coq_False () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_False ())
-let build_coq_True () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_True ())
-let build_coq_I () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_I ())
+let new_global sigma gr =
+  let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr
+  in Sigma.to_evar_map sigma, c
+    
+let build_coq_False sigma = new_global sigma (build_coq_False ())
+let build_coq_True sigma = new_global sigma (build_coq_True ())
+let build_coq_I sigma = new_global sigma (build_coq_I ())
 
 let rec build_discriminator env sigma dirn c = function
   | [] ->
       let ind = get_type_of env sigma c in
-      let true_0,false_0 =
-        build_coq_True(),build_coq_False() in
+      let sigma, true_0 = build_coq_True sigma in
+      let sigma, false_0 = build_coq_False sigma in
       build_selector env sigma dirn c ind true_0 false_0
   | ((sp,cnum),argnum)::l ->
+      let sigma, false_0 = build_coq_False sigma in
       let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
       let newc = mkRel(cnum_nlams-argnum) in
-      let subval = build_discriminator cnum_env sigma dirn newc l in
-      kont subval (build_coq_False (),mkSort (Prop Null))
+      let sigma, subval = build_discriminator cnum_env sigma dirn newc l in
+      kont sigma subval (false_0,mkSort (Prop Null))
 
 (* Note: discrimination could be more clever: if some elimination is
    not allowed because of a large impredicative constructor in the
@@ -991,9 +996,9 @@ let ind_scheme_of_eq lbeq =
 
 
 let discrimination_pf env sigma e (t,t1,t2) discriminator lbeq =
-  let i            = build_coq_I () in
-  let absurd_term  = build_coq_False () in
-  let eq_elim, eff = ind_scheme_of_eq lbeq in
+  let sigma, i           = build_coq_I sigma in
+  let sigma, absurd_term = build_coq_False sigma in
+  let eq_elim, eff       = ind_scheme_of_eq lbeq in
   let sigma, eq_elim = Evd.fresh_global (Global.env ()) sigma eq_elim in
   let eq_elim = EConstr.of_constr eq_elim in
     sigma, (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term),
@@ -1013,7 +1018,7 @@ let apply_on_clause (f,t) clause =
 let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
   let e = next_ident_away eq_baseid (ids_of_context env) in
   let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in
-  let discriminator =
+  let sigma, discriminator =
     build_discriminator e_env sigma dirn (mkVar e) cpath in
   let sigma,(pf, absurd_term), eff = 
     discrimination_pf env sigma e (t,t1,t2) discriminator lbeq in
@@ -1309,7 +1314,8 @@ let rec build_injrec env sigma dflt c = function
       let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
       let newc = mkRel(cnum_nlams-argnum) in
       let sigma, (subval,tuplety,dfltval) = build_injrec cnum_env sigma dflt newc l in
-	sigma, (kont subval (dfltval,tuplety), tuplety,dfltval)
+      let sigma, res = kont sigma subval (dfltval,tuplety) in
+      sigma, (res, tuplety,dfltval)
     with
 	UserError _ -> failwith "caught"
 
@@ -1326,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 *)
@@ -1346,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/equality.mli b/tactics/equality.mli
index b47be3bbc..27be5affb 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -126,4 +126,4 @@ val set_eq_dec_scheme_kind : mutual scheme_kind -> unit
 (* [build_selector env sigma i c t u v] matches on [c] of
    type [t] and returns [u] in branch [i] and [v] on other branches *)
 val build_selector : env -> evar_map -> int -> constr -> types ->
-  constr -> constr -> constr
+  constr -> constr -> evar_map * constr
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 35fbec5a6..2ba18ceb4 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 b443a357a..6e45739ec 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