diff options
Diffstat (limited to 'tactics/rewrite.ml4')
| -rw-r--r-- | tactics/rewrite.ml4 | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index ad8517c32a..dc59005f68 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1606,7 +1606,7 @@ let declare_instance_trans global binders a aeq n lemma = let declare_relation ?(binders=[]) a aeq n refl symm trans = init_setoid (); - let global = not (Locality.use_section_locality ()) in + let global = not (Locality.make_section_locality (Locality.LocalityFixme.consume ())) 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 @@ -1864,16 +1864,16 @@ let add_morphism glob binders m s n = VERNAC COMMAND EXTEND AddSetoid1 [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> - [ add_setoid (not (Locality.use_section_locality ())) [] a aeq t n ] + [ add_setoid (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] a aeq t n ] | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> - [ add_setoid (not (Locality.use_section_locality ())) binders a aeq t n ] + [ add_setoid (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders a aeq t n ] | [ "Add" "Morphism" constr(m) ":" ident(n) ] -> - [ add_morphism_infer (not (Locality.use_section_locality ())) m n ] + [ add_morphism_infer (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) m n ] | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] -> - [ add_morphism (not (Locality.use_section_locality ())) [] m s n ] + [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] m s n ] | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] -> - [ add_morphism (not (Locality.use_section_locality ())) binders m s n ] + [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders m s n ] END (** Bind to "rewrite" too *) |