diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/g_tactic.mlg | 8 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 2 |
2 files changed, 6 insertions, 4 deletions
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 46ea3819ac..7bf705ffeb 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -287,10 +287,10 @@ GRAMMAR EXTEND Gram [ [ c = smart_global; nl = occs -> { (nl,c) } ] ] ; intropatterns: - [ [ l = LIST0 nonsimple_intropattern -> { l } ] ] + [ [ l = LIST0 intropattern -> { l } ] ] ; ne_intropatterns: - [ [ l = LIST1 nonsimple_intropattern -> { l } ] ] + [ [ l = LIST1 intropattern -> { l } ] ] ; or_and_intropattern: [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> { IntroOrPattern tc } @@ -317,7 +317,7 @@ GRAMMAR EXTEND Gram | "?" -> { IntroAnonymous } | id = ident -> { IntroIdentifier id } ] ] ; - nonsimple_intropattern: + intropattern: [ [ l = simple_intropattern -> { l } | "*" -> { CAst.make ~loc @@ IntroForthcoming true } | "**" -> { CAst.make ~loc @@ IntroForthcoming false } ] ] @@ -534,6 +534,8 @@ GRAMMAR EXTEND Gram { TacAtom (CAst.make ~loc @@ TacIntroPattern (false,[CAst.make ~loc @@IntroForthcoming false])) } | IDENT "eintros"; pl = ne_intropatterns -> { TacAtom (CAst.make ~loc @@ TacIntroPattern (true,pl)) } + | IDENT "eintros" -> + { TacAtom (CAst.make ~loc @@ TacIntroPattern (true,[CAst.make ~loc @@IntroForthcoming false])) } | IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ","; inhyp = in_hyp_as -> { TacAtom (CAst.make ~loc @@ TacApply (true,false,cl,inhyp)) } diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 4bb52f599a..2055b25ff4 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -2014,7 +2014,7 @@ let add_morphism atts binders m s n = in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in ignore(new_instance ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance - (Some (true, CAst.make @@ CRecord [])) + None ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) (** Bind to "rewrite" too *) |