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.

1 files changed, 6 insertions, 5 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