Removing some goal unsafeness in inductive schemes.

9 files changed, 75 insertions, 35 deletions

diff --git a/engine/sigma.ml b/engine/sigma.ml
index e3e83b602..e886b0d1e 100644
--- a/engine/sigma.ml
+++ b/engine/sigma.ml
@@ -36,6 +36,18 @@ let new_evar sigma ?naming info =
 let define evk c sigma =
   Sigma ((), Evd.define evk c sigma, ())
 
+let fresh_sort_in_family ?rigid env sigma s =
+  let (sigma, s) = Evd.fresh_sort_in_family ?rigid env sigma s in
+  Sigma (s, sigma, ())
+
+let fresh_constant_instance env sigma cst =
+  let (sigma, cst) = Evd.fresh_constant_instance env sigma cst in
+  Sigma (cst, sigma, ())
+
+let fresh_inductive_instance env sigma ind =
+  let (sigma, ind) = Evd.fresh_inductive_instance env sigma ind in
+  Sigma (ind, sigma, ())
+
 let fresh_constructor_instance env sigma pc =
   let (sigma, c) = Evd.fresh_constructor_instance env sigma pc in
   Sigma (c, sigma, ())
diff --git a/engine/sigma.mli b/engine/sigma.mli
index 6ac56bb3e..cb948dba5 100644
--- a/engine/sigma.mli
+++ b/engine/sigma.mli
@@ -66,6 +66,12 @@ val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma
 
 (** Polymorphic universes *)
 
+val fresh_sort_in_family : ?rigid:Evd.rigid -> Environ.env ->
+  'r t -> Term.sorts_family -> (Term.sorts, 'r) sigma
+val fresh_constant_instance :
+  Environ.env -> 'r t -> constant -> (pconstant, 'r) sigma
+val fresh_inductive_instance :
+  Environ.env -> 'r t -> inductive -> (pinductive, 'r) sigma
 val fresh_constructor_instance : Environ.env -> 'r t -> constructor ->
   (pconstructor, 'r) sigma
 
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index c47602bda..bbe2f1a3a 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -12,6 +12,7 @@ open Tactics
 open Indfun_common
 open Functional_principles_proofs
 open Misctypes
+open Sigma.Notations
 
 exception Toberemoved_with_rel of int*constr
 exception Toberemoved
@@ -648,12 +649,15 @@ let build_case_scheme fa =
     let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
     List.assoc_f Constant.equal (fst (destConst funs)) this_block_funs_indexes
   in
-  let ind_fun =
+  let (ind, sf) =
 	 let ind = first_fun_kn,funs_indexes in
 	   (ind,Univ.Instance.empty)(*FIXME*),prop_sort
   in
-  let sigma, scheme = 
-    (fun (ind,sf) -> Indrec.build_case_analysis_scheme_default env sigma ind sf)  ind_fun in
+  let sigma = Sigma.Unsafe.of_evar_map sigma in
+  let Sigma (scheme, sigma, _) = 
+      Indrec.build_case_analysis_scheme_default env sigma ind sf
+  in
+  let sigma = Sigma.to_evar_map sigma in
   let scheme_type =  (Typing.unsafe_type_of env sigma ) scheme in
   let sorts =
     (fun (_,_,x) ->
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 54d47fbe0..6dfc32bf1 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -28,6 +28,7 @@ open Inductiveops
 open Environ
 open Reductionops
 open Nametab
+open Sigma.Notations
 
 type dep_flag = bool
 
@@ -120,13 +121,14 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
       mkLambda_string "f" t
 	(add_branch (push_rel (Anonymous, None, t) env) (k+1))
   in
-  let sigma, s = Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env sigma kind in
+  let Sigma (s, sigma, p) = Sigma.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env sigma kind in
   let typP = make_arity env' dep indf s in
   let c = 
     it_mkLambda_or_LetIn_name env
     (mkLambda_string "P" typP
      (add_branch (push_rel (Anonymous,None,typP) env') 0)) lnamespar
-  in sigma, c
+  in
+  Sigma (c, sigma, p)
 
 (* check if the type depends recursively on one of the inductive scheme *)
 
@@ -474,7 +476,9 @@ let mis_make_indrec env sigma listdepkind mib u =
 	  it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind)
 	    lnamesparrec
       else
-	let evd', c = mis_make_case_com dep env !evdref (indi,u) (mibi,mipi) kind in
+        let sigma = Sigma.Unsafe.of_evar_map !evdref in
+        let Sigma (c, sigma, _) = mis_make_case_com dep env sigma (indi,u) (mibi,mipi) kind in
+        let evd' = Sigma.to_evar_map sigma in
 	  evdref := evd'; c
   in
     (* Body of mis_make_indrec *)
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index f616c9679..81416a322 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -25,13 +25,13 @@ type dep_flag = bool
 
 (** Build a case analysis elimination scheme in some sort family *)
 
-val build_case_analysis_scheme : env -> evar_map -> pinductive ->
-      dep_flag -> sorts_family -> evar_map * constr
+val build_case_analysis_scheme : env -> 'r Sigma.t -> pinductive ->
+      dep_flag -> sorts_family -> (constr, 'r) Sigma.sigma
 
 (** Build a dependent case elimination predicate unless type is in Prop *)
 
-val build_case_analysis_scheme_default : env -> evar_map -> pinductive ->
-      sorts_family -> evar_map * constr
+val build_case_analysis_scheme_default : env -> 'r Sigma.t -> pinductive ->
+      sorts_family -> (constr, 'r) Sigma.sigma
 
 (** Builds a recursive induction scheme (Peano-induction style) in the same
    sort family as the inductive family; it is dependent if not in Prop *)
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 8a6d93cf7..59cce19ef 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -18,6 +18,7 @@ open Indrec
 open Declarations
 open Typeops
 open Ind_tables
+open Sigma.Notations
 
 (* Induction/recursion schemes *)
 
@@ -102,10 +103,10 @@ let rec_dep_scheme_kind_from_type =
 
 let build_case_analysis_scheme_in_type dep sort ind =
   let env = Global.env () in
-  let sigma = Evd.from_env env in
-  let sigma, indu = Evd.fresh_inductive_instance env sigma ind in
-  let sigma, c = build_case_analysis_scheme env sigma indu dep sort in 
-    c, Evd.evar_universe_context sigma
+  let sigma = Sigma.Unsafe.of_evar_map (Evd.from_env env) in
+  let Sigma (indu, sigma, _) = Sigma.fresh_inductive_instance env sigma ind in
+  let Sigma (c, sigma, _) = build_case_analysis_scheme env sigma indu dep sort in
+    c, Evd.evar_universe_context (Sigma.to_evar_map sigma)
 
 let case_scheme_kind_from_type =
   declare_individual_scheme_object "_case_nodep"
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index b2603315d..76bf13a57 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -58,6 +58,7 @@ open Namegen
 open Inductiveops
 open Ind_tables
 open Indrec
+open Sigma.Notations
 
 let hid = Id.of_string "H"
 let xid = Id.of_string "X"
@@ -630,9 +631,10 @@ let fix_r2l_forward_rew_scheme (c, ctx') =
 (**********************************************************************)
  
 let build_r2l_rew_scheme dep env ind k =
-  let sigma, indu = Evd.fresh_inductive_instance env (Evd.from_env env) ind in
-  let sigma', c = build_case_analysis_scheme env sigma indu dep k in
-    c, Evd.evar_universe_context sigma'
+  let sigma = Sigma.Unsafe.of_evar_map (Evd.from_env env) in
+  let Sigma (indu, sigma, _) = Sigma.fresh_inductive_instance env sigma ind in
+  let Sigma (c, sigma, _) = build_case_analysis_scheme env sigma indu dep k in
+    c, Evd.evar_universe_context (Sigma.to_evar_map sigma)
 
 let build_l2r_rew_scheme = build_l2r_rew_scheme
 let build_l2r_forward_rew_scheme = build_l2r_forward_rew_scheme
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index bdbc0aa21..f2e013641 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -16,6 +16,7 @@ open Context
 open Declarations
 open Tacmach
 open Clenv
+open Sigma.Notations
 
 (************************************************************************)
 (* Tacticals re-exported from the Refiner module                        *)
@@ -225,12 +226,18 @@ let gl_make_elim ind gl =
     pf_apply Evd.fresh_global gl gr
 
 let gl_make_case_dep ind gl =
-  pf_apply Indrec.build_case_analysis_scheme gl ind true
+  let sigma = Sigma.Unsafe.of_evar_map (Tacmach.project gl) in
+  let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind true
     (elimination_sort_of_goal gl)
+  in
+  (Sigma.to_evar_map sigma, r)
 
 let gl_make_case_nodep ind gl =
-  pf_apply Indrec.build_case_analysis_scheme gl ind false
+  let sigma = Sigma.Unsafe.of_evar_map (Tacmach.project gl) in
+  let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind false
     (elimination_sort_of_goal gl)
+  in
+  (Sigma.to_evar_map sigma, r)
 
 let make_elim_branch_assumptions ba gl =
   let rec makerec (assums,cargs,constargs,recargs,indargs) lb lc =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 289d5109a..65d2749b5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1249,12 +1249,11 @@ let general_elim with_evars clear_flag (c, lbindc) elim =
 let general_case_analysis_in_context with_evars clear_flag (c,lbindc) =
   Proofview.Goal.nf_s_enter { s_enter = begin fun gl sigma ->
   let env = Proofview.Goal.env gl in
-  let sigma = Sigma.to_evar_map sigma in
   let concl = Proofview.Goal.concl gl in
-  let t = Retyping.get_type_of env sigma c in
-  let (mind,_) = reduce_to_quantified_ind env sigma t in
+  let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) c in
+  let (mind,_) = reduce_to_quantified_ind env (Sigma.to_evar_map sigma) t in
   let sort = Tacticals.New.elimination_sort_of_goal gl in
-  let sigma, elim =
+  let Sigma (elim, sigma, p) =
     if occur_term c concl then
       build_case_analysis_scheme env sigma mind true sort
     else
@@ -1264,7 +1263,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) =
    {elimindex = None; elimbody = (elim,NoBindings);
     elimrename = Some (false, constructors_nrealdecls (fst mind))})
   in
-  Sigma.Unsafe.of_pair (tac, sigma)
+  Sigma (tac, sigma, p)
   end }
 
 let general_case_analysis with_evars clear_flag (c,lbindc as cx) =
@@ -1444,8 +1443,9 @@ let descend_in_conjunctions avoid tac (err, info) c =
 	let elim =
 	  try DefinedRecord (Recordops.lookup_projections ind)
 	  with Not_found ->
-	    let elim = build_case_analysis_scheme env sigma (ind,u) false sort in
-	    NotADefinedRecordUseScheme (snd elim) in
+            let sigma = Sigma.Unsafe.of_evar_map sigma in
+	    let Sigma (elim, _, _) = build_case_analysis_scheme env sigma (ind,u) false sort in
+	    NotADefinedRecordUseScheme elim in
 	Tacticals.New.tclFIRST
 	  (List.init n (fun i ->
             Proofview.Goal.enter { enter = begin fun gl ->
@@ -3668,11 +3668,16 @@ let guess_elim isrec dep s hyp0 gl =
   let evd, elimc =
     if isrec && not (is_nonrec (fst mind)) then find_ind_eliminator (fst mind) s gl
     else
+      let env = Tacmach.New.pf_env gl in
+      let sigma = Sigma.Unsafe.of_evar_map (Tacmach.New.project gl) in
       if use_dependent_propositions_elimination () && dep
       then
-	Tacmach.New.pf_apply build_case_analysis_scheme gl mind true s
+        let Sigma (ind, sigma, _) = build_case_analysis_scheme env sigma mind true s in
+        (Sigma.to_evar_map sigma, ind)
       else
-	Tacmach.New.pf_apply build_case_analysis_scheme_default gl mind s in
+        let Sigma (ind, sigma, _) = build_case_analysis_scheme_default env sigma mind s in
+        (Sigma.to_evar_map sigma, ind)
+  in
   let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in
     evd, ((elimc, NoBindings), elimt), mkIndU mind
 
@@ -4025,10 +4030,9 @@ let induction_gen clear_flag isrec with_evars elim
   | _ -> [] in
   Proofview.Goal.enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
-  let sigma = Tacmach.New.project gl in
+  let sigma = Proofview.Goal.sigma gl in
   let ccl = Proofview.Goal.raw_concl gl in
   let cls = Option.default allHypsAndConcl cls in
-  let sigma = Sigma.Unsafe.of_evar_map sigma in
   let t = typ_of env sigma c in
   let is_arg_pure_hyp =
     isVar c && not (mem_named_context (destVar c) (Global.named_context()))
@@ -4251,11 +4255,11 @@ let elim_type t =
 
 let case_type t =
   Proofview.Goal.s_enter { s_enter = begin fun gl sigma ->
-  let (ind,t) = Tacmach.New.pf_apply reduce_to_atomic_ind gl t in
-  let evd, elimc =
-    Tacmach.New.pf_apply build_case_analysis_scheme_default gl ind (Tacticals.New.elimination_sort_of_goal gl)
-  in
-  Sigma.Unsafe.of_pair (elim_scheme_type elimc t, evd)
+  let env = Tacmach.New.pf_env gl in
+  let (ind,t) = reduce_to_atomic_ind env (Sigma.to_evar_map sigma) t in
+  let s = Tacticals.New.elimination_sort_of_goal gl in
+  let Sigma (elimc, evd, p) = build_case_analysis_scheme_default env sigma ind s in
+  Sigma (elim_scheme_type elimc t, evd, p)
   end }