diff options
Diffstat (limited to 'tactics/rewrite.ml')
| -rw-r--r-- | tactics/rewrite.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index b4e1683eb..aa0152d35 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1685,7 +1685,7 @@ let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance global binders instance fields = new_instance (Flags.is_universe_polymorphism ()) - binders instance (Some (CRecord (Loc.ghost,None,fields))) + binders instance (Some (true, CRecord (Loc.ghost,None,fields))) ~global ~generalize:false None let declare_instance_refl global binders a aeq n lemma = @@ -1895,7 +1895,8 @@ let add_morphism glob binders m s n = [cHole; s; m])) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - ignore(new_instance ~global:glob poly binders instance (Some (CRecord (Loc.ghost,None,[]))) + ignore(new_instance ~global:glob poly binders instance + (Some (true, CRecord (Loc.ghost,None,[]))) ~generalize:false ~tac ~hook:(declare_projection n instance_id) None) (** Bind to "rewrite" too *) |