diff options
| author | Maxime Dénès | 2017-11-24 12:46:57 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-24 12:46:57 +0100 |
| commit | 31794a1828a15acb95c235fd3166c511635add41 (patch) | |
| tree | fb09a6b201001ababc3030dc80fa9d729526c0a7 /plugins/ltac/rewrite.ml | |
| parent | 92c15a9b660b874ce3fa125b1f9bdf2e85c40f47 (diff) | |
| parent | 57f62f06419972ba799e451d2f56552dc1b2fb63 (diff) | |
Merge PR #6197: [plugin] Remove LocalityFixme über hack.
Diffstat (limited to 'plugins/ltac/rewrite.ml')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index c63492d1be..14b0742a76 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1800,9 +1800,9 @@ let declare_instance_trans global binders a aeq n lemma = in anew_instance global binders instance [(Ident (Loc.tag @@ Id.of_string "transitivity"),lemma)] -let declare_relation ?(binders=[]) a aeq n refl symm trans = +let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = init_setoid (); - let global = not (Locality.make_section_locality (Locality.LocalityFixme.consume ())) in + let global = not (Locality.make_section_locality locality) in let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" in ignore(anew_instance global binders instance []); match (refl,symm,trans) with |