From 3ef3e0d145c2765c17e0f10b9c0d896c09365662 Mon Sep 17 00:00:00 2001 From: msozeau Date: Sat, 30 Jan 2010 15:26:23 +0000 Subject: Update CHANGES, add documentation for new commands/tactics and do a bit of cleanup in tactics/ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12705 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Sorting/Permutation.v | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) (limited to 'theories/Sorting') diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index da30d096c..c3cd4f4a8 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -75,11 +75,10 @@ Hint Resolve Permutation_refl Permutation_sym Permutation_trans. (* This provides reflexivity, symmetry and transitivity and rewriting on morphims to come *) -Add Parametric Relation A : (list A) (@Permutation A) - reflexivity proved by (@Permutation_refl A) - symmetry proved by (@Permutation_sym A) - transitivity proved by (@Permutation_trans A) -as Permutation_Equivalence. +Instance Permutation_Equivalence A : Equivalence (@Permutation A) | 10 := { + Equivalence_Reflexive := @Permutation_refl A ; + Equivalence_Symmetric := @Permutation_sym A ; + Equivalence_Transitive := @Permutation_trans A }. Add Parametric Morphism A (a:A) : (cons a) with signature @Permutation A ==> @Permutation A -- cgit v1.2.3