From 4eafa8d4cc44da82f528cf61508330a6a28355b2 Mon Sep 17 00:00:00 2001 From: sacerdot Date: Fri, 1 Oct 2004 16:33:00 +0000 Subject: The "Add Setoid" command now has a new argument "as name" that is used to generate the name of the morphism. Previously the name was automatically generated, but this behaviour was not compatible with module typing: it was not possible to generate the same identifier in the module type and in the module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6168 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/ring/Setoid_ring_normalize.v | 2 +- contrib/ring/Setoid_ring_theory.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'contrib') diff --git a/contrib/ring/Setoid_ring_normalize.v b/contrib/ring/Setoid_ring_normalize.v index 6e46c3f33..2a2ec3720 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 7166a6372..efed61102 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. -- cgit v1.2.3