| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
| |
pas correctes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10739 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
gratuit, je me suis décidé pour quelque chose de plus atomique).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10379 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
( ('a -> 'b -> bool) -> 'a option -> 'b option -> bool devient la même
chose mais avec 'a='b ) et de contenu pour avoir une sémantique plus
claire.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10353 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
devient Flags.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
tout cassé hier sans m'en rendre compte (le soucis de travailler sur un
ordinateur où j'ai pas installé lablgtk2).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10347 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
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
|
herbelin
aspiwack