diff options
| author |  clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-03-14 14:40:34 +0000 |
|---|---|---|
| committer | clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-03-14 14:40:34 +0000 |
| commit | 3f81d0083aec1311095b4bf540c21dbe5156b7ba (patch) | |
| tree | ee71437ca0df8f7b8359e8ecb55a46e470764865 /contrib/ring/ring.ml | |
| parent | d04cfb111916c3a7082a75a51e9883e8a5a45a51 (diff) | |
reparation semi setoid ring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2531 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/ring/ring.ml')
| -rw-r--r-- | contrib/ring/ring.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index 83ed2ad14..dabf68892 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -153,7 +153,7 @@ module OperSet = type morph = { plusm : constr; multm : constr; - oppm : constr; + oppm : constr option; } type theory = @@ -340,7 +340,7 @@ let _ = (Some { plusm = (constr_of pm); multm = (constr_of mm); - oppm = (constr_of om)}) + oppm = Some (constr_of om)}) (constr_of aplus) (constr_of amult) (constr_of aone) @@ -356,7 +356,7 @@ let _ = (function | (VARG_CONSTR a)::(VARG_CONSTR aequiv)::(VARG_CONSTR asetth)::(VARG_CONSTR aplus) ::(VARG_CONSTR amult)::(VARG_CONSTR aone)::(VARG_CONSTR azero) - ::(VARG_CONSTR aeq)::(VARG_CONSTR pm)::(VARG_CONSTR mm)::(VARG_CONSTR om) + ::(VARG_CONSTR aeq)::(VARG_CONSTR pm)::(VARG_CONSTR mm) ::(VARG_CONSTR t)::l -> (fun () -> (add_theory false false true (constr_of a) @@ -365,7 +365,7 @@ let _ = (Some { plusm = (constr_of pm); multm = (constr_of mm); - oppm = (constr_of om)}) + oppm = None}) (constr_of aplus) (constr_of amult) (constr_of aone) @@ -720,7 +720,7 @@ let build_setpolynom gl th lc = th.th_mult; th.th_one; th.th_zero;(unbox th.th_opp); th.th_eq; v; th.th_t; (unbox th.th_setoid_th); (unbox th.th_morph).plusm; (unbox th.th_morph).multm; - (unbox th.th_morph).oppm; p |]))) + (unbox (unbox th.th_morph).oppm); p |]))) lp (* |