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/funind | |
| 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/funind')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 1 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 1 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 1 |
3 files changed, 3 insertions, 0 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index f37cb3ed03..6df9d574f9 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 233cdddd7f..dd475315c7 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 c65d3181c3..55ebd31b93 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));; |