From 7e1fefc0a095f7bb7f720218f9d472d4b0d6507d Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Mon, 12 Dec 2011 14:00:45 +0000
Subject: Proof using ...

New vernacular "Proof using idlist" to declare the variables
to be discharged at the end of the current proof. The system
checks that the set of declared variables is a superset of
the set of actually used variables.

It can be combined in a single line with "Proof with":
Proof with .. using ..
Proof using .. with ..

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14789 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/leminv.ml   | 1 +
 tactics/rewrite.ml4 | 3 ++-
 tactics/tactics.ml  | 3 ++-
 3 files changed, 5 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index a6915461d7..1697c14654 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -235,6 +235,7 @@ let add_inversion_lemma name env sigma t sort dep inv_op =
     declare_constant name
     (DefinitionEntry
        { const_entry_body = invProof;
+         const_entry_secctx = None;
          const_entry_type = None;
          const_entry_opaque = false },
      IsProof Lemma)
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 805f4260a7..80930af42c 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1647,6 +1647,7 @@ let declare_projection n instance_id r =
   let typ = it_mkProd_or_LetIn typ ctx in
   let cst =
     { const_entry_body = term;
+      const_entry_secctx = None;
       const_entry_type = Some typ;
       const_entry_opaque = false }
   in
@@ -1713,7 +1714,7 @@ let add_morphism_infer glob m n =
   let instance = build_morphism_signature m in
     if Lib.is_modtype () then
       let cst = Declare.declare_constant ~internal:Declare.KernelSilent instance_id
-				(Entries.ParameterEntry (instance,None), Decl_kinds.IsAssumption Decl_kinds.Logical)
+				(Entries.ParameterEntry (None,instance,None), Decl_kinds.IsAssumption Decl_kinds.Logical)
       in
 	add_instance (Typeclasses.new_instance (Lazy.force proper_class) None glob (ConstRef cst));
 	declare_projection n instance_id (ConstRef cst)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 25a148bbdb..45eee91eef 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3516,7 +3516,8 @@ let admit_as_an_axiom gl =
   let concl = it_mkNamedProd_or_LetIn (pf_concl gl) sign in
   if occur_existential concl then error"\"admit\" cannot handle existentials.";
   let axiom =
-    let cd = Entries.ParameterEntry (concl,None) in
+    let cd = 
+      Entries.ParameterEntry (Pfedit.get_used_variables(),concl,None) in
     let con = Declare.declare_constant ~internal:Declare.KernelSilent na (cd,IsAssumption Logical) in
     constr_of_global (ConstRef con)
   in
-- 
cgit v1.2.3