diff options
-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). |