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

4 files changed, 32 insertions, 16 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 28f11c9af4..a4485fac7f 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -56,12 +56,13 @@ type mutual_inductive_entry = {
 
 type definition_entry = {
   const_entry_body   : constr;
+  const_entry_secctx : section_context option;
   const_entry_type   : types option;
   const_entry_opaque : bool }
 
 type inline = int option (* inlining level, None for no inlining *)
 
-type parameter_entry = types * inline
+type parameter_entry = section_context option * types * inline 
 
 type constant_entry =
   | DefinitionEntry of definition_entry
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 08740afae7..b726d0ec0d 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -52,12 +52,13 @@ type mutual_inductive_entry = {
 
 type definition_entry = {
   const_entry_body   : constr;
+  const_entry_secctx : section_context option;
   const_entry_type   : types option;
   const_entry_opaque : bool }
 
 type inline = int option (* inlining level, None for no inlining *)
 
-type parameter_entry = types * inline
+type parameter_entry = section_context option * types * inline 
 
 type constant_entry =
   | DefinitionEntry of definition_entry
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index cc9366c116..478b9c6fc6 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -102,11 +102,11 @@ let infer_declaration env dcl =
 	then OpaqueDef (Declarations.opaque_from_val j.uj_val)
 	else Def (Declarations.from_val j.uj_val)
       in
-      def, typ, cst
-  | ParameterEntry (t,nl) ->
+      def, typ, cst, c.const_entry_secctx
+  | ParameterEntry (ctx,t,nl) ->
       let (j,cst) = infer env t in
       let t = hcons_constr (Typeops.assumption_of_judgment env j) in
-      Undef nl, NonPolymorphicType t, cst
+      Undef nl, NonPolymorphicType t, cst, ctx
 
 let global_vars_set_constant_type env = function
   | NonPolymorphicType t -> global_vars_set env t
@@ -116,14 +116,26 @@ let global_vars_set_constant_type env = function
 	  (fun t c -> Idset.union (global_vars_set env t) c))
       ctx ~init:Idset.empty
 
-let build_constant_declaration env kn (def,typ,cst) =
-  let ids_typ = global_vars_set_constant_type env typ in
-  let ids_def = match def with
-    | Undef _ -> Idset.empty
-    | Def cs -> global_vars_set env (Declarations.force cs)
-    | OpaqueDef lc -> global_vars_set env (Declarations.force_opaque lc)
-  in
-  let hyps = keep_hyps env (Idset.union ids_typ ids_def) in
+let build_constant_declaration env kn (def,typ,cst,ctx) =
+  let hyps = 
+    let inferred =
+      let ids_typ = global_vars_set_constant_type env typ in
+      let ids_def = match def with
+      | Undef _ -> Idset.empty
+      | Def cs -> global_vars_set env (Declarations.force cs)
+      | OpaqueDef lc -> 
+          global_vars_set env (Declarations.force_opaque lc) in
+      keep_hyps env (Idset.union ids_typ ids_def) in
+    let declared = match ctx with
+      | None -> inferred 
+      | Some declared -> declared in
+    let mk_set l = List.fold_right Idset.add (List.map pi1 l) Idset.empty in
+    let inferred_set, declared_set = mk_set inferred, mk_set declared in
+    if not (Idset.subset inferred_set declared_set) then
+      error ("The following section variable are used but not declared:\n"^
+        (String.concat ", " (List.map string_of_id
+          (Idset.elements (Idset.diff inferred_set declared_set)))));
+    declared in
   let tps = Cemitcodes.from_val (compile_constant_body env def) in
   { const_hyps = hyps;
     const_body = def;
@@ -137,7 +149,8 @@ let translate_constant env kn ce =
   build_constant_declaration env kn (infer_declaration env ce)
 
 let translate_recipe env kn r =
-  build_constant_declaration env kn (Cooking.cook_constant env r)
+  build_constant_declaration env kn 
+    (let def,typ,cst = Cooking.cook_constant env r in def,typ,cst,None)
 
 (* Insertion of inductive types. *)
 
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 158f2c7877..3bbf566774 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -22,10 +22,11 @@ val translate_local_assum : env -> types ->
   types * Univ.constraints
 
 val infer_declaration : env -> constant_entry ->
-  constant_def * constant_type * constraints
+  constant_def * constant_type * constraints * Sign.section_context option
 
 val build_constant_declaration : env -> 'a ->
-  constant_def * constant_type * constraints -> constant_body
+  constant_def * constant_type * constraints * Sign.section_context option -> 
+    constant_body
 
 val translate_constant : env -> constant -> constant_entry -> constant_body