diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/g_tactic.mlg | 8 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 3 |
2 files changed, 6 insertions, 5 deletions
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 1b00a93834..eb282d1f83 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -439,7 +439,7 @@ GRAMMAR EXTEND Gram [ [ "in"; id = id_or_meta; ipat = as_ipat -> { Some (id,ipat) } | -> { None } ] ] ; - orient: + orient_rw: [ [ "->" -> { true } | "<-" -> { false } | -> { true } ] ] @@ -451,10 +451,10 @@ GRAMMAR EXTEND Gram ] ] ; fixdecl: - [ [ "("; id = ident; bl=LIST0 simple_binder; ann=fixannot; + [ [ "("; id = ident; bl=LIST0 simple_binder; ann=struct_annot; ":"; ty=lconstr; ")" -> { (loc, id, bl, ann, ty) } ] ] ; - fixannot: + struct_annot: [ [ "{"; IDENT "struct"; id=name; "}" -> { Some id } | -> { None } ] ] ; @@ -506,7 +506,7 @@ GRAMMAR EXTEND Gram ] ] ; oriented_rewriter : - [ [ b = orient; p = rewriter -> { let (m,c) = p in (b,m,c) } ] ] + [ [ b = orient_rw; p = rewriter -> { let (m,c) = p in (b,m,c) } ] ] ; induction_clause: [ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat; diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 1493092f2f..6be358be21 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -2023,7 +2023,8 @@ let add_morphism atts binders m s n = let _id, lemma = Classes.new_instance_interactive ~global:atts.global ~poly:atts.polymorphic instance_name binders instance_t - ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info + ~generalize:false ~tac ~hook:(declare_projection n instance_id) + Hints.empty_hint_info None in lemma (* no instance body -> always open proof *) |