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

6 files changed, 10 insertions, 3 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index f37cb3ed03..6df9d574f9 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -381,6 +381,7 @@ let generate_functional_principle
 	(*       Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
 	let ce =
 	  { const_entry_body = value;
+            const_entry_secctx = None;
 	    const_entry_type = None;
 	    const_entry_opaque = false }
 	in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 233cdddd7f..dd475315c7 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -158,6 +158,7 @@ let definition_message id =
 
 let save with_clean id const (locality,kind) hook =
   let {const_entry_body = pft;
+       const_entry_secctx = _;
        const_entry_type = tpo;
        const_entry_opaque = opacity } = const in
   let l,r = match locality with
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index c65d3181c3..55ebd31b93 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1131,6 +1131,7 @@ let (value_f:constr list -> global_reference -> constr) =
 let (declare_fun : identifier -> logical_kind -> constr -> global_reference) =
   fun f_id kind value ->
     let ce = {const_entry_body = value;
+              const_entry_secctx = None;
 	      const_entry_type = None;
 	      const_entry_opaque = false } in
       ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index d189a4e55c..9d61c06de6 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -158,6 +158,7 @@ let ty c = Typing.type_of (Global.env()) Evd.empty c
 let decl_constant na c =
   mkConst(declare_constant (id_of_string na) (DefinitionEntry
     { const_entry_body = c;
+      const_entry_secctx = None;
       const_entry_type = None;
       const_entry_opaque = true },
     IsProof Lemma))
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index f02e83ad1a..ecae6759f0 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -325,7 +325,8 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
 	let body = it_mkLambda_or_LetIn (mkApp (constr_of_global gr, [|make|])) binders_rel in
 	let ty = it_mkProd_or_LetIn top_arity binders_rel in
 	let ce =
-	  { const_entry_body = Evarutil.nf_evar !isevars body;
+          { const_entry_body = Evarutil.nf_evar !isevars body;
+            const_entry_secctx = None;
 	    const_entry_type = Some ty;
 	    const_entry_opaque = false }
 	in 
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index a719a9f9af..64d9f72cae 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -248,6 +248,7 @@ let declare_definition prg =
   let (local, kind) = prg.prg_kind in
   let ce =
     { const_entry_body = body;
+      const_entry_secctx = None;
       const_entry_type = Some typ;
       const_entry_opaque = false }
   in
@@ -347,6 +348,7 @@ let declare_obligation prg obl body =
       let opaque = if get_proofs_transparency () then false else opaque in
       let ce = 
 	{ const_entry_body = body;
+          const_entry_secctx = None;
 	  const_entry_type = Some ty;
 	  const_entry_opaque = opaque }
       in
@@ -661,8 +663,8 @@ let admit_obligations n =
 	match x.obl_body with
 	| None ->
             let x = subst_deps_obl obls x in
-	    let kn = Declare.declare_constant x.obl_name (ParameterEntry (x.obl_type,None),
-							 IsAssumption Conjectural) 
+	    let kn = Declare.declare_constant x.obl_name 
+              (ParameterEntry (None, x.obl_type,None), IsAssumption Conjectural)
 	    in
 	      assumption_message x.obl_name;
 	      obls.(i) <- { x with obl_body = Some (mkConst kn) }