diff options
| author | gareuselesinge | 2011-12-12 14:00:45 +0000 |
|---|---|---|
| committer | gareuselesinge | 2011-12-12 14:00:45 +0000 |
| commit | 7e1fefc0a095f7bb7f720218f9d472d4b0d6507d (patch) | |
| tree | a853d983f64e85d752d771df1e8f2044879a6ca2 /plugins/subtac | |
| parent | dc8f9bb9033702dc7552450c5a3891fd060ee001 (diff) | |
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
Diffstat (limited to 'plugins/subtac')
| -rw-r--r-- | plugins/subtac/subtac_command.ml | 3 | ||||
| -rw-r--r-- | plugins/subtac/subtac_obligations.ml | 6 |
2 files changed, 6 insertions, 3 deletions
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) } |