From 23f4804b50307766219392229757e75da9aa41d9 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 18 Jun 2014 17:16:59 +0200
Subject: 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.

---
 plugins/Derive/derive.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'plugins/Derive')

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
-- 
cgit v1.2.3