diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-11 20:14:31 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-11 20:14:31 +0000 |
| commit | 4425c8d353ffdcbed966c253f9624b550626ae0a (patch) | |
| tree | 13e25097ff2865f00dabd37cf3ed6a5748f20e32 /plugins | |
| parent | 180a27f8d2b7ba2d7913c37ae01c946acb8c813e (diff) | |
Added a Local Definition vernacular command. This type of definition
has to be refered through its qualified name even when the module
containing it is imported.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16263 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 3 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 19 |
2 files changed, 12 insertions, 10 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index debf96345..7f05c3b0e 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -348,8 +348,7 @@ let generate_functional_principle Declare.declare_constant name (Entries.DefinitionEntry ce, - Decl_kinds.IsDefinition (Decl_kinds.Scheme) - ) + Decl_kinds.IsDefinition (Decl_kinds.Scheme)) ); Declare.definition_message name; names := name :: !names diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 9879f08a0..8305c4735 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -148,25 +148,28 @@ open Declare let definition_message = Declare.definition_message +let get_locality = function +| Discharge -> true +| Local -> true +| Global -> false + 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 - | Local when Lib.sections_are_opened () -> + | Discharge when Lib.sections_are_opened () -> let k = Kindops.logical_kind_of_goal_kind kind in let c = SectionLocalDef (pft, tpo, opacity) in let _ = declare_variable id (Lib.cwd(), c, k) in (Local, VarRef id) - | Local -> - let k = Kindops.logical_kind_of_goal_kind kind in - let kn = declare_constant id (DefinitionEntry const, k) in - (Global, ConstRef kn) - | Global -> + | Discharge | Local | Global -> + let local = get_locality locality in let k = Kindops.logical_kind_of_goal_kind kind in - let kn = declare_constant id (DefinitionEntry const, k) in - (Global, ConstRef kn) in + let kn = declare_constant id ~local (DefinitionEntry const, k) in + (locality, ConstRef kn) + in if with_clean then Pfedit.delete_current_proof (); hook l r; definition_message id |