diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:08:09 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:08:09 +0000 |
| commit | 442feb2c07f8f5824e814bba504f02c2742637e2 (patch) | |
| tree | 25a45991d4c52b9265820cbb52137b1c92ad52cd /tactics/rewrite.ml4 | |
| parent | bf7cfcf92c45af9f559f5bf004e9730d96921850 (diff) | |
Vernacexpr is now a mli-only file, locality stuff now in locality.ml
Adds a directory ./intf for pure interfaces.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15367 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/rewrite.ml4')
| -rw-r--r-- | tactics/rewrite.ml4 | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 458c5bec6..88170d6dd 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1477,7 +1477,7 @@ let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance global binders instance fields = new_instance binders instance (Some (CRecord (dummy_loc,None,fields))) - ~global:(not (Vernacexpr.use_section_locality ())) ~generalize:false None + ~global:(not (Locality.use_section_locality ())) ~generalize: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" @@ -1496,7 +1496,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 (Vernacexpr.use_section_locality ()) in + let global = not (Locality.use_section_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 @@ -1754,16 +1754,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 (Vernacexpr.use_section_locality ())) [] a aeq t n ] + [ add_setoid (not (Locality.use_section_locality ())) [] a aeq t n ] | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> - [ add_setoid (not (Vernacexpr.use_section_locality ())) binders a aeq t n ] + [ add_setoid (not (Locality.use_section_locality ())) binders a aeq t n ] | [ "Add" "Morphism" constr(m) ":" ident(n) ] -> - [ add_morphism_infer (not (Vernacexpr.use_section_locality ())) m n ] + [ add_morphism_infer (not (Locality.use_section_locality ())) m n ] | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] -> - [ add_morphism (not (Vernacexpr.use_section_locality ())) [] m s n ] + [ add_morphism (not (Locality.use_section_locality ())) [] m s n ] | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] -> - [ add_morphism (not (Vernacexpr.use_section_locality ())) binders m s n ] + [ add_morphism (not (Locality.use_section_locality ())) binders m s n ] END (** Bind to "rewrite" too *) |