diff options
| author | Matthieu Sozeau | 2014-06-11 16:55:29 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-11 16:55:29 +0200 |
| commit | 99cdbc25a3a92545544a087ed55240c488b42fc9 (patch) | |
| tree | 4b9f80d7ae15a421b5745dec138759a37cf68da6 /tactics | |
| parent | 1c620d266885086e076011917d5b1d28af299ea1 (diff) | |
Fix bug #3289
Diffstat (limited to 'tactics')
| -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 b4e1683eb8..aa0152d35a 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 *) |