diff options
| -rw-r--r-- | contrib/ring/Setoid_ring_normalize.v | 2 | ||||
| -rw-r--r-- | contrib/ring/Setoid_ring_theory.v | 2 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 5 |
3 files changed, 5 insertions, 4 deletions
diff --git a/contrib/ring/Setoid_ring_normalize.v b/contrib/ring/Setoid_ring_normalize.v index 6e46c3f331..2a2ec37207 100644 --- a/contrib/ring/Setoid_ring_normalize.v +++ b/contrib/ring/Setoid_ring_normalize.v @@ -34,7 +34,7 @@ Variable Aeq : A -> A -> bool. Variable S : Setoid_Theory A Aequiv. -Add Setoid A Aequiv S. +Add Setoid A Aequiv S as Asetoid. Variable plus_morph : diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v index 7166a63727..efed611021 100644 --- a/contrib/ring/Setoid_ring_theory.v +++ b/contrib/ring/Setoid_ring_theory.v @@ -22,7 +22,7 @@ Infix Local "==" := Aequiv (at level 70, no associativity). Variable S : Setoid_Theory A Aequiv. -Add Setoid A Aequiv S. +Add Setoid A Aequiv S as Asetoid. Variable Aplus : A -> A -> A. Variable Amult : A -> A -> A. diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index ff12e366cf..f182570a5f 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -195,11 +195,12 @@ TACTIC EXTEND SetoidRewrite END VERNAC COMMAND EXTEND AddSetoid1 - [ "Add" "Setoid" constr(a) constr(aeq) constr(t) ] -> [ add_setoid a aeq t ] + [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> + [ add_setoid n a aeq t ] | [ "Add" "Morphism" constr(m) ":" ident(n) ] -> [ new_named_morphism n m None ] | [ "Add" "Morphism" constr(m) "with" "signature" morphism_signature(s) "as" ident(n) ] -> - [ new_named_morphism n m (Some s)] + [ new_named_morphism n m (Some s)] END VERNAC COMMAND EXTEND AddRelation1 |