From b163cf2480615bce4bf280df6c5490f558eb3405 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 3 Jun 2015 22:08:45 +0200
Subject: Admitted does not drop poly-univ constraints (Fix #4244)

---
 proofs/proof_global.ml  | 2 +-
 proofs/proof_global.mli | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 3e2c813e38..50a68952eb 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -74,7 +74,7 @@ type proof_object = {
 }
 
 type proof_ending =
-  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry
+  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes
   | Proved of Vernacexpr.opacity_flag *
              (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
               proof_object
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 9d5038a3f9..6a5116a9e7 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -66,7 +66,7 @@ type proof_object = {
 }
 
 type proof_ending =
-  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry
+  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes
   | Proved of Vernacexpr.opacity_flag *
              (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
               proof_object
-- 
cgit v1.2.3