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

1 files changed, 7 insertions, 3 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index fff6eb6fa2..ffb1130ebb 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -62,7 +62,7 @@ let red_constant_entry n ce = function
   | Some red ->
       let body = ce.const_entry_body in
       { ce with const_entry_body =
-	under_binders (Global.env()) (fst (reduction_of_red_expr red)) n body }
+        under_binders (Global.env()) (fst (reduction_of_red_expr red)) n body }
 
 let interp_definition bl red_option c ctypopt =
   let env = Global.env() in
@@ -77,6 +77,7 @@ let interp_definition bl red_option c ctypopt =
 	check_evars env Evd.empty !evdref body;
 	imps1@(Impargs.lift_implicits nb_args imps2),
 	{ const_entry_body = body;
+          const_entry_secctx = None;
 	  const_entry_type = None;
           const_entry_opaque = false }
     | Some ctyp ->
@@ -88,6 +89,7 @@ let interp_definition bl red_option c ctypopt =
 	check_evars env Evd.empty !evdref typ;
 	imps1@(Impargs.lift_implicits nb_args imps2),
 	{ const_entry_body = body;
+          const_entry_secctx = None;
 	  const_entry_type = Some typ;
           const_entry_opaque = false }
   in
@@ -112,7 +114,7 @@ let declare_definition ident (local,k) ce imps hook =
   let r = match local with
     | Local when Lib.sections_are_opened () ->
         let c =
-          SectionLocalDef(ce.const_entry_body,ce.const_entry_type,false) in
+          SectionLocalDef(ce.const_entry_body ,ce.const_entry_type,false) in
         let _ = declare_variable ident (Lib.cwd(),c,IsDefinition k) in
         definition_message ident;
         if Pfedit.refining () then
@@ -140,7 +142,8 @@ let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) =
 	  Typeclasses.declare_instance None true r; r
     | (Global|Local) ->
         let kn =
-          declare_constant ident (ParameterEntry (c,nl), IsAssumption kind) in
+          declare_constant ident 
+            (ParameterEntry (None,c,nl), IsAssumption kind) in
 	let gr = ConstRef kn in
 	  maybe_declare_manual_implicits false gr imps;
         assumption_message ident;
@@ -474,6 +477,7 @@ let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
 let declare_fix kind f def t imps =
   let ce = {
     const_entry_body = def;
+    const_entry_secctx = None;
     const_entry_type = Some t;
     const_entry_opaque = false }
   in