diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-28 01:41:09 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-28 01:41:09 +0000 |
| commit | abc3a74c095ec62e761de253cbd6e7b9080ad604 (patch) | |
| tree | aa9c7dad1b3c18ea04d1226050e4f9535ede44e8 /contrib/ring | |
| parent | d334f75272a29dae279ce5ef48f3dc9f3026ddb5 (diff) | |
Nettoyage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3317 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/ring')
| -rw-r--r-- | contrib/ring/Ring_normalize.v | 9 | ||||
| -rw-r--r-- | contrib/ring/Setoid_ring_normalize.v | 9 |
2 files changed, 0 insertions, 18 deletions
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v index 34f4aeea9..4e6317ace 100644 --- a/contrib/ring/Ring_normalize.v +++ b/contrib/ring/Ring_normalize.v @@ -338,15 +338,6 @@ Unset Implicit Arguments. (* Section properties. *) -(************** -Syntax constr - level 0: - fix_cache [<<Fix $x{$_[$_:$_]:$_:=$_}>>] -> [ "Fix " $x ] -| fix_cache2 [<<Fix $x{$_[$_:$_;$_:$_]:$_:=$_}>>] -> [ "Fix " $x ] -| fix_cache3 [<<Fix $x{$_[$_:$_;$_:$_;$_:$_]:$_:=$_}>>] -> [ "Fix " $x ] -. -************) - Variable T : (Semi_Ring_Theory Aplus Amult Aone Azero Aeq). Hint SR_plus_sym_T := Resolve (SR_plus_sym T). diff --git a/contrib/ring/Setoid_ring_normalize.v b/contrib/ring/Setoid_ring_normalize.v index ec5f32fc2..085ff557d 100644 --- a/contrib/ring/Setoid_ring_normalize.v +++ b/contrib/ring/Setoid_ring_normalize.v @@ -352,15 +352,6 @@ Unset Implicit Arguments. (* Section properties. *) -(************** -Syntax constr - level 0: - fix_cache [<<Fix $x{$_[$_:$_]:$_:=$_}>>] -> [ "Fix " $x ] -| fix_cache2 [<<Fix $x{$_[$_:$_;$_:$_]:$_:=$_}>>] -> [ "Fix " $x ] -| fix_cache3 [<<Fix $x{$_[$_:$_;$_:$_;$_:$_]:$_:=$_}>>] -> [ "Fix " $x ] -. -************) - Variable T : (Semi_Setoid_Ring_Theory A Aequiv Aplus Amult Aone Azero Aeq). Hint SSR_plus_sym_T := Resolve (SSR_plus_sym T). |