Proofs now take and return an evar_universe_context, simplifying interfaces

and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml.
The context produced by typechecking a statement is passed in the proof, allowing the
universe name context to be correctly folded as well. Mainly an API cleanup.

5 files changed, 23 insertions, 18 deletions

diff --git a/plugins/Derive/derive.ml b/plugins/Derive/derive.ml
index 160e905f8c..1601a7ce2e 100644
--- a/plugins/Derive/derive.ml
+++ b/plugins/Derive/derive.ml
@@ -15,7 +15,7 @@ let interp_init_def_and_relation env sigma init_def r =
     mkProd (Names.Anonymous,init_type, mkProd (Names.Anonymous,init_type,mkProp))
   in
   let r, ctx = Constrintern.interp_casted_constr sigma env r r_type in
-  init_def , init_type , r, Evd.evar_universe_context_set ctx
+  init_def , init_type , r, ctx
   
 
 (** [start_deriving f init r lemma] starts a proof of [r init
@@ -23,14 +23,15 @@ let interp_init_def_and_relation env sigma init_def r =
     [lemma] as the proof. *)
 let start_deriving f init_def r lemma =
   let env = Global.env () in
+  let sigma = Evd.from_env env in
   let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in
   let ( init_def , init_type , r , ctx ) =
-    interp_init_def_and_relation env Evd.empty init_def r
+    interp_init_def_and_relation env sigma init_def r
   in
   let goals =
     let open Proofview in
-    TCons ( env , (init_type , ctx ) , (fun ef ->
-      TCons ( env , ( Term.mkApp ( r , [| init_def ; ef |] ) , Univ.ContextSet.empty) , (fun _ -> TNil))))
+    TCons ( env , (init_type ) , (fun ef ->
+      TCons ( env , ( Term.mkApp ( r , [| init_def ; ef |] )) , (fun _ -> TNil))))
   in
   let terminator com =
     let open Proof_global in
@@ -65,7 +66,7 @@ let start_deriving f init_def r lemma =
         ignore (Declare.declare_constant lemma lemma_def)
   in
   let () = Proof_global.start_dependent_proof
-    lemma kind goals terminator
+    lemma kind ctx goals terminator
   in
   let _ = Proof_global.with_current_proof begin fun _ p ->
     Proof.run_tactic env Proofview.(tclFOCUS 1 1 shelve) p
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 9589e51f43..841796ed76 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -987,8 +987,9 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
       i*)
     (mk_equation_id f_id)
     (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem))
-    (lemma_type, (*FIXME*) Univ.ContextSet.empty)
-    (Lemmas.mk_hook (fun _ _ -> ()));
+  Evd.empty_evar_universe_context
+  lemma_type
+  (Lemmas.mk_hook (fun _ _ -> ()));
   ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
   Lemmas.save_proof (Vernacexpr.Proved(false,None))
 
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 8c3033d0c2..c4a340880e 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -278,7 +278,8 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
     Lemmas.start_proof
       new_princ_name
       (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem))
-      (new_principle_type, (*FIXME*) Univ.ContextSet.empty)
+      (*FIXME*) Evd.empty_evar_universe_context
+    new_principle_type
       hook
     ;
     (*       let _tim1 = System.get_time ()  in *)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 20304b529a..52d3b4a87b 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1079,7 +1079,8 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	 let lem_id = mk_correct_id f_id in
 	 Lemmas.start_proof lem_id
 	   (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem))
-           (fst lemmas_types_infos.(i), (*FIXME*)Univ.ContextSet.empty)
+                 (*FIXME*) Evd.empty_evar_universe_context
+	 (fst lemmas_types_infos.(i))
            (Lemmas.mk_hook (fun _ _ -> ()));
 	 ignore (Pfedit.by
 	   (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
@@ -1132,7 +1133,8 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	 let lem_id = mk_complete_id f_id in
 	 Lemmas.start_proof lem_id
 	   (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem))
-           (fst lemmas_types_infos.(i), (*FIXME*)Univ.ContextSet.empty)
+                            (*FIXME*) Evd.empty_evar_universe_context
+	 (fst lemmas_types_infos.(i))
            (Lemmas.mk_hook (fun _ _ -> ()));
 	 ignore (Pfedit.by
 	   (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 961266c9c4..f141d3619c 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1269,7 +1269,7 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos
     let lid = ref [] in
     let h_num = ref (-1) in
     Proof_global.discard_all ();
-    build_proof (Univ.ContextSet.empty)
+    build_proof Evd.empty_evar_universe_context
       (  fun gls ->
 	   let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
 	   tclTHENSEQ
@@ -1317,7 +1317,7 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos
   Lemmas.start_proof
     na
     (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma)
-    (gls_type, ctx)
+    ctx gls_type
     (Lemmas.mk_hook hook);
   if Indfun_common.is_strict_tcc  ()
   then
@@ -1360,12 +1360,11 @@ let com_terminate
     thm_name using_lemmas
     nb_args ctx
     hook =
-  let ctx = Univ.ContextSet.of_context ctx in
   let start_proof ctx (tac_start:tactic) (tac_end:tactic) =
     let (evmap, env) = Lemmas.get_current_context() in
     Lemmas.start_proof thm_name
       (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env)
-      (compute_terminate_type nb_args fonctional_ref, ctx) hook;
+      ctx (compute_terminate_type nb_args fonctional_ref) hook;
 
     ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start)));
     ignore (by (Proofview.V82.tactic (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref
@@ -1374,7 +1373,7 @@ let com_terminate
   start_proof ctx tclIDTAC tclIDTAC;
   try
     let sigma, new_goal_type = build_new_goal_type () in
-    open_new_goal start_proof (Evd.universe_context_set sigma)
+    open_new_goal start_proof (Evd.evar_universe_context sigma)
       using_lemmas tcc_lemma_ref
       (Some tcc_lemma_name)
       (new_goal_type);
@@ -1414,7 +1413,8 @@ let (com_eqn : int -> Id.t ->
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
     (Lemmas.start_proof eq_name (Global, false, Proof Lemma)
        ~sign:(Environ.named_context_val env)
-       (equation_lemma_type, (*FIXME*)Univ.ContextSet.empty)
+       (Evd.evar_universe_context evmap)
+       equation_lemma_type
        (Lemmas.mk_hook (fun _ _ -> ()));
      ignore (by
        (Proofview.V82.tactic (start_equation f_ref terminate_ref
@@ -1481,8 +1481,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let equation_id = add_suffix function_name "_equation" in
   let functional_id =  add_suffix function_name "_F" in
   let term_id = add_suffix function_name "_terminate" in
-  let ctx = Evd.universe_context evm in
-  let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res in
+  let ctx = Evd.evar_universe_context evm in
+  let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(Evd.universe_context evm) res in
   let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in  
   let relation =
     fst (*FIXME*)(interp_constr