diff options
| author | Pierre-Marie Pédrot | 2016-04-09 17:14:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-04-09 17:14:18 +0200 |
| commit | bb43730ac876b8de79967090afa50f00858af6d5 (patch) | |
| tree | 8d96531b4869f9ab1e0cd00064f4dbab96cd4ac8 /ltac | |
| parent | b5420538da04984ca42eb4284a9be27f3b5ba021 (diff) | |
| parent | 84f079fa31723b6a97edc50ca7a81e1eb19e759c (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/rewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index cf2a01052f..97b2393a8d 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -1749,7 +1749,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 (true, CRecord (Loc.ghost,fields))) - ~global ~generalize:false None + ~global ~generalize:false ~refine:false None let declare_instance_refl global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" |