Equality cleanup: remove constr_of_global

3 files changed, 27 insertions, 20 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index b3017f359..43c06a54d 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -231,9 +231,9 @@ let make_prb gls depth additionnal_terms =
 let build_projection intype (cstr:pconstructor) special default gls=
   let open Tacmach.New in
   let ci= (snd(fst cstr)) in
-  let body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in
+  let sigma, body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in
   let id=pf_get_new_id (Id.of_string "t") gls in
-    mkLambda(Name id,intype,body)
+  sigma, mkLambda(Name id,intype,body)
 
 (* generate an adhoc tactic following the proof tree  *)
 
@@ -346,12 +346,13 @@ let rec proof_tac p : unit Proofview.tactic =
 	 let special=mkRel (1+nargs-argind) in
 	 refresh_universes (type_of ti) (fun intype ->
          refresh_universes (type_of default) (fun outtype ->
-         let proj =
+         let sigma, proj =
            build_projection intype cstr special default gl
          in
 	 let injt=
            app_global_with_holes _f_equal [|intype;outtype;proj;ti;tj|] 1 in
-	   Tacticals.New.tclTHEN injt (proof_tac prf)))
+	 Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+                               (Tacticals.New.tclTHEN injt (proof_tac prf))))
   with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end }
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index e6278943d..b48d60a4f 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"
 
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