From fb75bd254df2eadfc8abd45a646dfe9b1c4a53b6 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Wed, 5 Dec 2007 21:11:19 +0000 Subject: 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 --- parsing/ppconstr.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'parsing/ppconstr.ml') diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 1c9eb1e2a2..8e542ce147 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -386,12 +386,12 @@ let pr_fixdecl pr prd dangling_with_for (id,(n,ro),bl,t,c) = match ro with CStructRec -> if List.length ids > 1 && n <> None then - spc() ++ str "{struct " ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}" + spc() ++ str "{struct " ++ pr_name (snd (List.nth ids (Option.get n))) ++ str"}" else mt() | CWfRec c -> - spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}" + spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids (Option.get n))) ++ str"}" | CMeasureRec c -> - spc () ++ str "{measure " ++ pr lsimple c ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}" + spc () ++ str "{measure " ++ pr lsimple c ++ pr_name (snd (List.nth ids (Option.get n))) ++ str"}" in pr_recursive_decl pr prd dangling_with_for id bl annot t c @@ -428,7 +428,7 @@ let pr_case_item pr (tm,(na,indnalopt)) = | Name id when not (is_var id tm) -> spc () ++ str "as " ++ pr_id id | Anonymous when tm_clash (tm,indnalopt) <> None -> (* hide [tm] name to avoid conflicts *) - spc () ++ str "as _" (* ++ pr_id (out_some (tm_clash (tm,indnalopt)))*) + spc () ++ str "as _" (* ++ pr_id (Option.get (tm_clash (tm,indnalopt)))*) | _ -> mt ()) ++ *) (match na with (* Decision of printing "_" or not moved to constrextern.ml *) -- cgit v1.2.3