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

11 files changed, 42 insertions, 13 deletions

diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index 79ae41c1d..9258a39fc 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -179,7 +179,8 @@ let declare_record_instance gr ctx params =
   let ident = make_instance_ident gr in
   let def = it_mkLambda_or_LetIn (applistc (constr_of_global gr) params) ctx in
   let def = deep_refresh_universes def in
-  let ce = { const_entry_body=def;
+  let ce = { const_entry_body= def;
+             const_entry_secctx = None;
 	     const_entry_type=None;
 	     const_entry_opaque=false } in
   let cst = Declare.declare_constant ident
@@ -194,8 +195,9 @@ let declare_class_instance gr ctx params =
   let def = deep_refresh_universes def in
   let typ = deep_refresh_universes typ in
   let ce = Entries.DefinitionEntry
-    {  const_entry_type=Some typ;
-       const_entry_body=def;
+    {  const_entry_type = Some typ;
+       const_entry_secctx = None;
+       const_entry_body= def;
        const_entry_opaque=false } in
   try
   let cst = Declare.declare_constant ident
diff --git a/toplevel/class.ml b/toplevel/class.ml
index e977959d2..ebaa19b66 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -219,6 +219,7 @@ let build_id_coercion idf_opt source =
   let constr_entry = (* Cast is necessary to express [val_f] is identity *)
     DefinitionEntry
       { const_entry_body = mkCast (val_f, DEFAULTcast, typ_f);
+        const_entry_secctx = None;
 	const_entry_type = Some typ_f;
         const_entry_opaque = false } in
   let kn = declare_constant idf (constr_entry,IsDefinition IdentityCoercion) in
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 61d7d31d7..1e83e4b81 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -110,6 +110,7 @@ let declare_instance_constant k pri global imps ?hook id term termtype =
     let kind = IsDefinition Instance in
     let entry =
       { const_entry_body   = term;
+        const_entry_secctx = None;
 	const_entry_type   = Some termtype;
 	const_entry_opaque = false }
     in DefinitionEntry entry, kind
@@ -182,7 +183,8 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 	in
 	Evarutil.check_evars env Evd.empty !evars termtype;
 	let cst = Declare.declare_constant ~internal:Declare.KernelSilent id
-	  (Entries.ParameterEntry (termtype,None), Decl_kinds.IsAssumption Decl_kinds.Logical)
+	  (Entries.ParameterEntry 
+            (None,termtype,None), Decl_kinds.IsAssumption Decl_kinds.Logical)
 	in instance_hook k None global imps ?hook (ConstRef cst); id
       end
     else
@@ -297,7 +299,7 @@ let context l =
   let fn (id, _, t) =
     if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
       let cst = Declare.declare_constant ~internal:Declare.KernelSilent id
-	(ParameterEntry (t,None), IsAssumption Logical)
+	(ParameterEntry (None,t,None), IsAssumption Logical)
       in
 	match class_of_constr t with
 	| Some (rels, (tc, args) as _cl) ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index fff6eb6fa..ffb1130eb 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
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 9d0f17ee7..e43a23c95 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -204,7 +204,7 @@ let rec attribute_of_vernac_command = function
   | VernacUnfocus -> [SolveCommand]
   | VernacShow _ -> [OtherStatePreservingCommand]
   | VernacCheckGuard -> [OtherStatePreservingCommand]
-  | VernacProof (Tacexpr.TacId []) -> [OtherStatePreservingCommand]
+  | VernacProof (None, None) -> [OtherStatePreservingCommand]
   | VernacProof _ -> []
 
   | VernacProofMode _ -> []
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 30c537f28..de3b62f82 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -125,6 +125,7 @@ let define internal id c =
   let kn = fd id
     (DefinitionEntry
       { const_entry_body = c;
+        const_entry_secctx = None;
         const_entry_type = None;
         const_entry_opaque = false },
       Decl_kinds.IsDefinition Scheme) in
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index e3779e131..d346f422e 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -110,6 +110,7 @@ let define id internal c t =
   let kn = f id
     (DefinitionEntry
       { const_entry_body = c;
+        const_entry_secctx = None;
         const_entry_type = t;
         const_entry_opaque = false },
       Decl_kinds.IsDefinition Scheme) in
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 5817ef1b9..6f344db58 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -199,7 +199,7 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) =
           (Local,VarRef id,imps)
       | Global ->
           let k = IsAssumption Conjectural in
-          let kn = declare_constant id (ParameterEntry (t_i,None), k) in
+          let kn = declare_constant id (ParameterEntry (None,t_i,None), k) in
           (Global,ConstRef kn,imps))
   | Some body ->
       let k = logical_kind_of_goal_kind kind in
@@ -215,6 +215,7 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) =
       | Global ->
           let const =
             { const_entry_body = body_i;
+              const_entry_secctx = None;
               const_entry_type = Some t_i;
               const_entry_opaque = opaq } in
           let kn = declare_constant id (DefinitionEntry const, k) in
@@ -328,8 +329,9 @@ let start_proof_com kind thms hook =
 
 let admit () =
   let (id,k,typ,hook) = Pfedit.current_proof_statement () in
+  let e = Pfedit.get_used_variables(), typ, None in
   let kn =
-    declare_constant id (ParameterEntry (typ,None),IsAssumption Conjectural) in
+    declare_constant id (ParameterEntry e,IsAssumption Conjectural) in
   Pfedit.delete_current_proof ();
   assumption_message id;
   hook Global (ConstRef kn)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index ee190d350..86849cbbb 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -203,6 +203,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
 	        try
 		  let cie = {
 		    const_entry_body = proj;
+                    const_entry_secctx = None;
                     const_entry_type = Some projtyp;
                     const_entry_opaque = false } in
 		  let k = (DefinitionEntry cie,IsDefinition kind) in
@@ -312,6 +313,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
 	let class_type = Option.map (fun ar -> it_mkProd_or_LetIn ar params) arity in
 	let class_entry =
 	  { const_entry_body = class_body;
+            const_entry_secctx = None;
 	    const_entry_type = class_type;
 	    const_entry_opaque = false }
 	in
@@ -323,6 +325,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
 	let proj_body = it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in
 	let proj_entry =
 	  { const_entry_body = proj_body;
+            const_entry_secctx = None;
 	    const_entry_type = Some proj_type;
 	    const_entry_opaque = false }
 	in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 110e6190c..435d85233 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -674,6 +674,15 @@ let vernac_set_end_tac tac =
   if tac <> (Tacexpr.TacId []) then set_end_tac (Tacinterp.interp tac) else ()
     (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
 
+let vernac_set_used_variables l =
+  let l = List.map snd l in
+  if not (list_distinct l) then error "Used variables list contains duplicates";
+  let vars = Environ.named_context (Global.env ()) in
+  List.iter (fun id -> 
+    if not (List.exists (fun (id',_,_) -> id = id') vars) then
+      error ("Unknown variable: " ^ string_of_id id))
+    l;
+  set_used_variables l
 
 (*****************************)
 (* Auxiliary file management *)
@@ -1514,7 +1523,11 @@ let interp c = match c with
   | VernacEndSubproof -> vernac_end_subproof ()
   | VernacShow s -> vernac_show s
   | VernacCheckGuard -> vernac_check_guard ()
-  | VernacProof tac -> vernac_set_end_tac tac
+  | VernacProof (None, None) -> ()
+  | VernacProof (Some tac, None) -> vernac_set_end_tac tac
+  | VernacProof (None, Some l) -> vernac_set_used_variables l
+  | VernacProof (Some tac, Some l) -> 
+      vernac_set_end_tac tac; vernac_set_used_variables l
   | VernacProofMode mn -> Proof_global.set_proof_mode mn
   (* Toplevel control *)
   | VernacToplevelControl e -> raise e
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 33a474923..b1ab3bdce 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -357,7 +357,7 @@ type vernac_expr =
   | VernacEndSubproof
   | VernacShow of showable
   | VernacCheckGuard
-  | VernacProof of raw_tactic_expr
+  | VernacProof of raw_tactic_expr option * lident list option
   | VernacProofMode of string
   (* Toplevel control *)
   | VernacToplevelControl of exn