Factorisation des opérations sur le type option de Util dans un module

lib/option.ml(i) . J'en profite pour rajouter des primitives de lifting 
des fonctions (à un ou deux arguments tous ou partie de type option).

Il reste quelques opérations dans Util à propos desquelles je ne suis 
pas trop sûr, ou simplement que j'ai oublié, mais qui attendront demain 
car il est tard (comme some_in qui devrait devenir Option.make je 
suppose) . Elles s'expriment souvent facilement en fonction des 
autres, par exemple "option_compare x y"  est égal à "Option.lift2 compare x y"
. Le option_cons devrait faire son chemin dans le module parce qu'il est 
assez primitif et qu'il n'y a pas de fonction "cons" dans OCaml.

J'en ai profité aussi pour remplacer les trop nombreux "failwith" par 
des erreurs locales au module, donc plus robustes.

J'ai trouvé aussi une fonction qui était définie deux fois, et une 
définie dans un module particulier.

Mon seul bémol (mais facile à traiter) c'est la proximité entre le 
nom de module Option et l'ancien Options. J'ai pas de meilleure idée de 
nom à l'heure qu'il est, ni pour l'un, ni pour l'autre.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10346 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 5 deletions

diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index e81c9ddd5..97dd2f143 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -193,7 +193,7 @@ let _ =
 let subst_morph subst morph = 
   let plusm' = subst_mps subst morph.plusm in
   let multm' = subst_mps subst morph.multm in
-  let oppm' = option_smartmap (subst_mps subst) morph.oppm in
+  let oppm' = Option.smartmap (subst_mps subst) morph.oppm in
     if plusm' == morph.plusm 
       && multm' == morph.multm 
       && oppm' == morph.oppm then 
@@ -215,15 +215,15 @@ let subst_set subst cset =
     if !same then cset else cset'
 
 let subst_theory subst th = 
-  let th_equiv' = option_smartmap (subst_mps subst) th.th_equiv in
-  let th_setoid_th' = option_smartmap (subst_mps subst) th.th_setoid_th in
-  let th_morph' = option_smartmap (subst_morph subst) th.th_morph in
+  let th_equiv' = Option.smartmap (subst_mps subst) th.th_equiv in
+  let th_setoid_th' = Option.smartmap (subst_mps subst) th.th_setoid_th in
+  let th_morph' = Option.smartmap (subst_morph subst) th.th_morph in
   let th_a' = subst_mps subst th.th_a in                   
   let th_plus' = subst_mps subst th.th_plus in
   let th_mult' = subst_mps subst th.th_mult in
   let th_one' = subst_mps subst th.th_one in
   let th_zero' = subst_mps subst th.th_zero in
-  let th_opp' = option_smartmap (subst_mps subst) th.th_opp in
+  let th_opp' = Option.smartmap (subst_mps subst) th.th_opp in
   let th_eq' = subst_mps subst th.th_eq in
   let th_t' = subst_mps subst th.th_t in          
   let th_closed' = subst_set subst th.th_closed in