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

36 files changed, 233 insertions, 44 deletions

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index c781c8274..e5dc669dd 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -133,6 +133,24 @@ one gulp, as a proof term (see Section~\ref{exact}).
 
 \SeeAlso {\tt Proof with {\tac}.} in Section~\ref{ProofWith}.
 
+\subsection[\tt Proof using {\ident$_1$ \dots {\ident$_n$}}.]
+{\tt Proof using {\ident$_1$ \dots {\ident$_n$}}.
+\comindex{Proof using} \label{ProofUsing}}
+
+This command applies in proof editing mode. 
+It declares the set of section variables (see~\ref{Variable}) 
+used by the proof. At {\tt Qed} time, the system will assert that 
+the set of section variables actually used in the proof is a subset of
+the declared one.
+
+The set of declared variables is closed under type dependency.
+For example if {\tt T} is variable and {\tt a} is a variable of
+type {\tt T}, the commands {\tt Proof using a} and
+{\tt Proof using T a} are actually equivalent.
+
+\variant {\tt Proof using {\ident$_1$ \dots {\ident$_n$}} with {\tac}.} 
+in Section~\ref{ProofWith}.
+
 \subsection[\tt Abort.]{\tt Abort.\comindex{Abort}}
 
 This command cancels the current proof development, switching back to
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index d0c193de1..198f8f304 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4239,6 +4239,16 @@ e.g. \texttt{Require Import A.}).
 
 \SeeAlso {\tt Proof.} in Section~\ref{BeginProof}.
 
+\begin{Variants}
+\item {\tt Proof with {\tac} using {\ident$_1$ \dots {\ident$_n$}}}
+  Combines in a single line {\tt Proof with} and {\tt Proof using}, 
+  see~\ref{ProofUsing}
+\item {\tt Proof using {\ident$_1$ \dots {\ident$_n$}} with {\tac}}
+  Combines in a single line {\tt Proof with} and {\tt Proof using}, 
+  see~\ref{ProofUsing}
+
+\end{Variants}
+
 \subsubsection[\tt Declare Implicit Tactic {\tac}.]{\tt Declare Implicit Tactic {\tac}.\comindex{Declare Implicit Tactic}}
 
 This command declares a tactic to be used to solve implicit arguments
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 28f11c9af..a4485fac7 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 08740afae..b726d0ec0 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 cc9366c11..478b9c6fc 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 158f2c787..3bbf56677 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
 
diff --git a/library/declare.ml b/library/declare.ml
index 0afd4bd9e..288580850 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -148,7 +148,7 @@ let discharge_constant ((sp,kn),(cdt,dhyps,kind)) =
   Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,kind)
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_constant_entry = ConstantEntry (ParameterEntry (mkProp,None))
+let dummy_constant_entry = ConstantEntry (ParameterEntry (None,mkProp,None))
 
 let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk
 
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 0f5d80a83..78299448a 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -34,9 +34,15 @@ GEXTEND Gram
   ;
   command:
     [ [ IDENT "Goal"; c = lconstr -> VernacGoal c
-      | IDENT "Proof" -> VernacProof (Tacexpr.TacId [])
-      | IDENT "Proof"; "with"; ta = tactic -> VernacProof ta
+      | IDENT "Proof" -> VernacProof (None,None)
       | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn
+      | IDENT "Proof"; "with"; ta = tactic; 
+        l = OPT [ "using"; l = LIST0 identref  -> l ] ->
+          VernacProof (Some ta, l)
+      | IDENT "Proof"; "using"; l = LIST0 identref; 
+        ta = OPT [ "with"; ta = tactic -> ta ] ->
+          VernacProof (ta,Some l)
+      | IDENT "Proof"; c = lconstr -> VernacExactProof c
       | IDENT "Abort" -> VernacAbort None
       | IDENT "Abort"; IDENT "All" -> VernacAbortAll
       | IDENT "Abort"; id = identref -> VernacAbort (Some id)
@@ -56,7 +62,6 @@ GEXTEND Gram
       | IDENT "Resume" -> VernacResume None
       | IDENT "Resume"; id = identref -> VernacResume (Some id)
       | IDENT "Restart" -> VernacRestart
-      | IDENT "Proof"; c = lconstr -> VernacExactProof c
       | IDENT "Undo" -> VernacUndo 1
       | IDENT "Undo"; n = natural -> VernacUndo n
       | IDENT "Undo"; IDENT "To"; n = natural -> VernacUndoTo n
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 27de53cad..e10d42b9d 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -972,9 +972,12 @@ let rec pr_vernac = function
 
   (* For extension *)
   | VernacExtend (s,c) -> pr_extend s c
-  | VernacProof (Tacexpr.TacId _) -> str "Proof"
-  | VernacProof te -> str "Proof with" ++ spc() ++ pr_raw_tactic te
-
+  | VernacProof (None, None) -> str "Proof"
+  | VernacProof (None, Some l) -> str "Proof using" ++spc()++ prlist pr_lident l
+  | VernacProof (Some te, None) -> str "Proof with" ++ spc() ++ pr_raw_tactic te
+  | VernacProof (Some te, Some l) -> 
+      str "Proof using" ++spc()++ prlist pr_lident l ++ spc() ++
+      str "with" ++ spc() ++pr_raw_tactic te
   | VernacProofMode s -> str ("Proof Mode "^s)
   | VernacSubproof None -> str "BeginSubproof"
   | VernacSubproof (Some i) -> str "BeginSubproof " ++ pr_int i
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index f37cb3ed0..6df9d574f 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 233cdddd7..dd475315c 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 c65d3181c..55ebd31b9 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 d189a4e55..9d61c06de 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 f02e83ad1..ecae6759f 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 a719a9f9a..64d9f72ca 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) }
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index e67c595bd..3d507f358 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -91,6 +91,11 @@ let set_end_tac tac =
   let tac = Proofview.V82.tactic tac in
   Proof_global.set_endline_tactic tac
 
+let set_used_variables l =
+  Proof_global.set_used_variables l
+let get_used_variables () =
+  Proof_global.get_used_variables ()
+
 exception NoSuchGoal
 let _ = Errors.register_handler begin function
   | NoSuchGoal -> Util.error "No such goal."
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 289e8c13c..7297b975f 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -154,6 +154,12 @@ val get_all_proof_names : unit -> identifier list
 val set_end_tac : tactic -> unit
 
 (** {6 ... } *)
+(** [set_used_variables l] declares that section variables [l] will be
+    used in the proof *)
+val set_used_variables : identifier list -> unit
+val get_used_variables : unit -> Sign.section_context option
+
+(** {6 ... } *)
 (** [solve_nth n tac] applies tactic [tac] to the [n]th subgoal of the
    current focused proof or raises a UserError if no proof is focused or
    if there is no [n]th subgoal *)
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 2aa31cd25..72730495d 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -119,6 +119,7 @@ type proof_state = {
 
 type proof_info = {
   mutable endline_tactic : unit Proofview.tactic ;
+  mutable section_vars : Sign.section_context option;
   initial_conclusions : Term.types list
 }
 
@@ -219,6 +220,11 @@ let _unfocus pr =
   pr.state <- { pr.state with proofview = Proofview.unfocus fc pr.state.proofview }
 
 
+let set_used_variables l p =
+  p.info.section_vars <- Some l
+
+let get_used_variables p = p.info.section_vars
+
 (*** Endline tactic ***)
 
 (* spiwack this is an information about the UI, it might be a good idea to move
@@ -364,7 +370,8 @@ let start goals =
       undo_stack = [] ;
       transactions = [] ;
       info = { endline_tactic = Proofview.tclUNIT ();
-	       initial_conclusions = List.map snd goals }
+               initial_conclusions = List.map snd goals;
+               section_vars = None }
     }
   in
   _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr;
diff --git a/proofs/proof.mli b/proofs/proof.mli
index d80ac79af..12af18f40 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -129,6 +129,9 @@ val get_proof_info : proof -> Store.t
 
 val set_proof_info : Store.t -> proof -> unit
 
+(* Sets the section variables assumed by the proof *)
+val set_used_variables : Sign.section_context -> proof -> unit
+val get_used_variables : proof -> Sign.section_context option
 
 (*** Endline tactic ***)
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index e9af46ba9..2745270a6 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -267,6 +267,16 @@ let set_endline_tactic tac =
   let p = give_me_the_proof () in
   Proof.set_endline_tactic tac p
 
+let set_used_variables l =
+  let p = give_me_the_proof () in
+  let env = Global.env () in
+  let ids = List.fold_right Idset.add l Idset.empty in
+  let ctx = Environ.keep_hyps env ids in
+  Proof.set_used_variables ctx p
+
+let get_used_variables () =
+  Proof.get_used_variables (give_me_the_proof ())
+
 let with_end_tac tac =
   let p = give_me_the_proof () in
   Proof.with_end_tac p tac
@@ -278,9 +288,11 @@ let close_proof () =
     let id = get_current_proof_name () in
     let p = give_me_the_proof () in
     let proofs_and_types = Proof.return p in
+    let section_vars = Proof.get_used_variables p in
     let entries = List.map
-      (fun (c,t) -> { Entries.const_entry_body = c ;
-                      const_entry_type  = Some t;
+      (fun (c,t) -> { Entries.const_entry_body = c;
+                      const_entry_secctx = section_vars;
+                      const_entry_type = Some t;
 		      const_entry_opaque = true })
       proofs_and_types
     in
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 2f9f4a549..ed6a60c71 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -82,6 +82,10 @@ val run_tactic : unit Proofview.tactic -> unit
 (** Sets the tactic to be used when a tactic line is closed with [...] *)
 val set_endline_tactic : unit Proofview.tactic -> unit
 
+(** Sets the section variables assumed by the proof *)
+val set_used_variables : Names.identifier list -> unit
+val get_used_variables : unit -> Sign.section_context option
+
 (** Appends the endline tactic of the current proof to a tactic. *)
 val with_end_tac : unit Proofview.tactic -> unit Proofview.tactic
 
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index a6915461d..1697c1465 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 805f4260a..80930af42 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 25a148bbd..45eee91ee 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
diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v
new file mode 100644
index 000000000..93a9ef116
--- /dev/null
+++ b/test-suite/success/proof_using.v
@@ -0,0 +1,61 @@
+Section Foo.
+
+Variable a : nat.
+
+Lemma l1 : True.
+Fail Proof using non_existing.
+Proof using a.
+exact I.
+Qed.
+
+Lemma l2 : True.
+Proof using a.
+Admitted.
+
+Lemma l3 : True.
+Proof using a.
+admit.
+Qed.
+
+End Foo.
+
+Check (l1 3).
+Check (l2 3).
+Check (l3 3).
+
+Section Bar.
+
+Variable T : Type.
+Variable a b : T.
+Variable H : a = b.
+
+Lemma l4 : a = b.
+Proof using H.
+exact H.
+Qed.
+
+End Bar.
+
+Check (l4 _ 1 1 _ : 1 = 1).
+
+Section S1.
+
+Variable v1 : nat.
+
+Section S2.
+
+Variable v2 : nat.
+
+Lemma deep : v1 = v2.
+Proof using v1 v2.
+admit.
+Qed.
+
+End S2.
+
+Check (deep 3 : v1 = 3).
+
+End S1.
+
+Check (deep 3 4 : 3 = 4).
+
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