diff options
| -rw-r--r-- | contrib/field/Field_Compl.v | 12 | ||||
| -rw-r--r-- | contrib/field/Field_Theory.v | 15 |
2 files changed, 12 insertions, 15 deletions
diff --git a/contrib/field/Field_Compl.v b/contrib/field/Field_Compl.v index 514edf39c0..edf0793176 100644 --- a/contrib/field/Field_Compl.v +++ b/contrib/field/Field_Compl.v @@ -22,10 +22,11 @@ Inductive Sprod [A:Type;B:Set] : Type := Spair : A -> B -> (Sprod A B). Definition assoc_2nd := -Fix assoc_2nd_rec {assoc_2nd_rec/4: - (A:Type)(B:Set)((e1,e2:B){e1=e2}+{~e1=e2})->(listT (Sprod A B))->B->A->A:= - [A:Type;B:Set;eq_dec:(e1,e2:B){e1=e2}+{~e1=e2};lst:(listT (Sprod A B)); - key:B;default:A] +Fix assoc_2nd_rec + {assoc_2nd_rec + [A:Type;B:Set;eq_dec:(e1,e2:B){e1=e2}+{~e1=e2};lst:(listT (Sprod A B))] + : B->A->A:= + [key:B;default:A] Cases lst of | nilT => default | (consT (Spair v e) l) => @@ -49,8 +50,7 @@ Definition sndT [A,B:Type;c:(prodT A B)] := end. Definition mem := -Fix mem {mem/4:(A:Set)((e1,e2:A){e1=e2}+{~e1=e2})->(a:A)(listT A)->bool := - [A:Set;eq_dec:(e1,e2:A){e1=e2}+{~e1=e2};a:A;l:(listT A)] +Fix mem {mem [A:Set;eq_dec:(e1,e2:A){e1=e2}+{~e1=e2};a:A;l:(listT A)] : bool := Cases l of | nilT => false | (consT a1 l1) => diff --git a/contrib/field/Field_Theory.v b/contrib/field/Field_Theory.v index fcd864f366..94e043dc84 100644 --- a/contrib/field/Field_Theory.v +++ b/contrib/field/Field_Theory.v @@ -207,9 +207,8 @@ Fixpoint interp_ExprA [lvar:(listT (Sprod AT nat));e:ExprA] : AT := (**** Associativity ****) Definition merge_mult := - Fix merge_mult {merge_mult/1:ExprA->ExprA->ExprA:= - [e1,e2:ExprA] - Cases e1 of + Fix merge_mult {merge_mult [e1:ExprA] : ExprA -> ExprA := + [e2:ExprA]Cases e1 of | (EAmult t1 t2) => Cases t2 of | (EAmult t2 t3) => (EAmult t1 (EAmult t2 (merge_mult t3 e2))) @@ -231,9 +230,8 @@ Fixpoint assoc_mult [e:ExprA] : ExprA := end. Definition merge_plus := - Fix merge_plus {merge_plus/1:ExprA->ExprA->ExprA:= - [e1,e2:ExprA] - Cases e1 of + Fix merge_plus {merge_plus [e1:ExprA]:ExprA->ExprA:= + [e2:ExprA]Cases e1 of | (EAplus t1 t2) => Cases t2 of | (EAplus t2 t3) => (EAplus t1 (EAplus t2 (merge_plus t3 e2))) @@ -401,9 +399,8 @@ Fixpoint distrib_EAopp [e:ExprA] : ExprA := end. Definition distrib_mult_right := - Fix distrib_mult_right {distrib_mult_right/1:ExprA->ExprA->ExprA:= - [e1,e2:ExprA] - Cases e1 of + Fix distrib_mult_right {distrib_mult_right [e1:ExprA]:ExprA->ExprA:= + [e2:ExprA]Cases e1 of | (EAplus t1 t2) => (EAplus (distrib_mult_right t1 e2) (distrib_mult_right t2 e2)) | _ => (EAmult e1 e2) |