diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-12 14:00:45 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-12 14:00:45 +0000 |
| commit | 7e1fefc0a095f7bb7f720218f9d472d4b0d6507d (patch) | |
| tree | a853d983f64e85d752d771df1e8f2044879a6ca2 /tactics/rewrite.ml4 | |
| 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 'tactics/rewrite.ml4')
| -rw-r--r-- | tactics/rewrite.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
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) |