diff options
| author |  clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-07-10 12:03:08 +0000 |
|---|---|---|
| committer | clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-07-10 12:03:08 +0000 |
| commit | 9c007d7d9744bababdb8b57da0a7ee7835bac434 (patch) | |
| tree | 2902f1610752a83a809cbf88a02bd1356b82bd65 /contrib/field/field.ml4 | |
| parent | d751d60b0511ff3daeb0bcd1384e3e982c410fa9 (diff) | |
Ajout d'un Ring pour setoides
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1839 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/field/field.ml4')
| -rw-r--r-- | contrib/field/field.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4 index 706b3a38d..19b8534d1 100644 --- a/contrib/field/field.ml4 +++ b/contrib/field/field.ml4 @@ -71,7 +71,7 @@ let add_field a aplus amult aone azero aopp aeq ainv aminus_o adiv_o rth ainv_l = begin (try - Ring.add_theory true true a aplus amult aone azero aopp aeq rth + Ring.add_theory true true false a None None None aplus amult aone azero (Some aopp) aeq rth Quote.ConstrSet.empty with | UserError("Add Semi Ring",_) -> ()); let th = mkApp ((constant ["Field_Theory"] "Build_Field_Theory"), |