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 /toplevel/record.ml | |
| 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 'toplevel/record.ml')
| -rw-r--r-- | toplevel/record.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index ee190d3506..86849cbbb2 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 |