From 57bee17f928fc67a599d2116edb42a59eeb21477 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 11 Oct 2013 18:30:54 +0200
Subject: Rework handling of universes on top of the STM, allowing for delayed
 computation in case of non-polymorphic proofs. Also fix plugins after
 forgotten merge conflicts. Still does not compile everything.

---
 tactics/leminv.ml  | 12 +-----------
 tactics/rewrite.ml | 13 +++++++++++++
 2 files changed, 14 insertions(+), 11 deletions(-)

(limited to 'tactics')

diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 23a7c9e532..81bc6a256c 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -228,17 +228,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
 
 let add_inversion_lemma name env sigma t sort dep inv_op =
   let invProof = inversion_scheme env sigma t sort dep inv_op in
-  let entry = {
-    const_entry_body = Future.from_val (invProof,Declareops.no_seff);
-    const_entry_secctx = None;
-    const_entry_type = None;
-    const_entry_proj = None;
-    const_entry_polymorphic = true;
-    const_entry_universes = Univ.UContext.empty (*FIXME *);
-    const_entry_opaque = false;
-    const_entry_inline_code = false;
-    const_entry_feedback = None;
-  } in
+  let entry = definition_entry ~poly:true (*FIXME*) invProof in
   let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in
   ()
 
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 83cb15f47e..cbf33fdb44 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -2130,3 +2130,16 @@ let myapply id l gl =
   in
     tclTHEN (Refiner.tclEVARS !evars) (apply app) gl
 
+let get_lemma_proof f env evm x y = 
+  let (evm, _), c = f env (evm,Evar.Set.empty) x y in
+    evm, c
+
+let get_reflexive_proof =
+  get_lemma_proof PropGlobal.get_reflexive_proof
+
+let get_symmetric_proof = 
+  get_lemma_proof PropGlobal.get_symmetric_proof
+
+let get_transitive_proof = 
+  get_lemma_proof PropGlobal.get_transitive_proof
+  
-- 
cgit v1.2.3