diff options
Diffstat (limited to 'contrib7')
-rw-r--r-- | contrib7/field/Field_Compl.v | 6 | ||||
-rw-r--r-- | contrib7/field/Field_Tactic.v | 8 | ||||
-rw-r--r-- | contrib7/field/Field_Theory.v | 4 |
3 files changed, 9 insertions, 9 deletions
diff --git a/contrib7/field/Field_Compl.v b/contrib7/field/Field_Compl.v index aa3a99147..8db3def83 100644 --- a/contrib7/field/Field_Compl.v +++ b/contrib7/field/Field_Compl.v @@ -57,6 +57,6 @@ Fix mem {mem [A:Set;eq_dec:(e1,e2:A){e1=e2}+{~e1=e2};a:A;l:(listT A)] : bool := end end}. -Inductive option [A:Type] : Type := - | None : (option A) - | Some : (A -> A -> A) -> (option A). +Inductive field_rel_option [A:Type] : Type := + | Field_None : (field_rel_option A) + | Field_Some : (A -> A -> A) -> (field_rel_option A). diff --git a/contrib7/field/Field_Tactic.v b/contrib7/field/Field_Tactic.v index cd382bc39..f15e5a4ce 100644 --- a/contrib7/field/Field_Tactic.v +++ b/contrib7/field/Field_Tactic.v @@ -236,10 +236,10 @@ Tactic Definition ApplySimplif sfun := Tactic Definition Unfolds FT := (Match Eval Cbv Beta Delta [Aminus] Iota in (Aminus FT) With - | [(Some ? ?1)] -> Unfold ?1 + | [(Field_Some ? ?1)] -> Unfold ?1 | _ -> Idtac); (Match Eval Cbv Beta Delta [Adiv] Iota in (Adiv FT) With - | [(Some ? ?1)] -> Unfold ?1 + | [(Field_Some ? ?1)] -> Unfold ?1 | _ -> Idtac). Tactic Definition Reduce FT := @@ -281,10 +281,10 @@ V7only [Tactic Definition field_gen := Field_Gen.]. Meta Definition InitExp FT trm := Let e = (Match Eval Cbv Beta Delta [Aminus] Iota in (Aminus FT) With - | [(Some ? ?1)] -> Eval Cbv Beta Delta [?1] in trm + | [(Field_Some ? ?1)] -> Eval Cbv Beta Delta [?1] in trm | _ -> trm) In Match Eval Cbv Beta Delta [Adiv] Iota in (Adiv FT) With - | [(Some ? ?1)] -> Eval Cbv Beta Delta [?1] in e + | [(Field_Some ? ?1)] -> Eval Cbv Beta Delta [?1] in e | _ -> e. V7only [ (*Used by contrib Maple *) diff --git a/contrib7/field/Field_Theory.v b/contrib7/field/Field_Theory.v index e2710260f..5af969756 100644 --- a/contrib7/field/Field_Theory.v +++ b/contrib7/field/Field_Theory.v @@ -21,8 +21,8 @@ Record Field_Theory : Type := Aopp : A -> A; Aeq : A -> A -> bool; Ainv : A -> A; - Aminus : (option A); - Adiv : (option A); + Aminus : (field_rel_option A); + Adiv : (field_rel_option A); RT : (Ring_Theory Aplus Amult Aone Azero Aopp Aeq); Th_inv_def : (n:A)~(n=Azero)->(Amult (Ainv n) n)=Aone }. |