diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-03 16:17:19 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-03 16:17:19 +0000 |
| commit | 2c91b948c37c333d45ff374f4d2845524c4600c1 (patch) | |
| tree | 18f29bfd0fdd6ab9d9dcb88c13261b5a14323641 /tactics/rewrite.ml4 | |
| parent | 249b1b6ccc4f3a25c675fcc5636924c4c9a25633 (diff) | |
Support globality flag properly for "Add Morphism foo : foo_mor" syntax.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12306 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/rewrite.ml4')
| -rw-r--r-- | tactics/rewrite.ml4 | 30 |
1 files changed, 15 insertions, 15 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index cff7e35eb..384ba3b93 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1236,24 +1236,24 @@ let add_morphism_infer glob m n = let instance = build_morphism_signature m in if Lib.is_modtype () then let cst = Declare.declare_internal_constant instance_id - (Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical) + (Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical) in - add_instance (Typeclasses.new_instance (Lazy.force proper_class) None glob cst); - declare_projection n instance_id (ConstRef cst) + add_instance (Typeclasses.new_instance (Lazy.force proper_class) None glob cst); + declare_projection n instance_id (ConstRef cst) else let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in - Flags.silently - (fun () -> - Command.start_proof instance_id kind instance - (fun _ -> function - Libnames.ConstRef cst -> - add_instance (Typeclasses.new_instance (Lazy.force proper_class) None - false cst); - declare_projection n instance_id (ConstRef cst) - | _ -> assert false); - Pfedit.by (Tacinterp.interp <:tactic< Coq.Classes.SetoidTactics.add_morphism_tactic>>)) (); - Flags.if_verbose (fun x -> msg (Printer.pr_open_subgoals x)) () - + Flags.silently + (fun () -> + Command.start_proof instance_id kind instance + (fun _ -> function + Libnames.ConstRef cst -> + add_instance (Typeclasses.new_instance (Lazy.force proper_class) None + glob cst); + declare_projection n instance_id (ConstRef cst) + | _ -> assert false); + Pfedit.by (Tacinterp.interp <:tactic< Coq.Classes.SetoidTactics.add_morphism_tactic>>)) (); + Flags.if_verbose (fun x -> msg (Printer.pr_open_subgoals x)) () + let add_morphism glob binders m s n = init_setoid (); let instance_id = add_suffix n "_Proper" in |