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

7 files changed, 57 insertions, 57 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index b10aa782c8..45976d6e5b 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -882,7 +882,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
   let f_def = Global.lookup_constant (destConst f) in
   let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
   let f_body =
-    force (out_some f_def.const_body)
+    force (Option.get f_def.const_body)
   in
   let params,f_body_with_params = decompose_lam_n nb_params f_body in
   let (_,num),(_,_,bodies) = destFix f_body_with_params in
@@ -933,8 +933,8 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
   let equation_lemma = 
     try 
       let finfos = find_Function_infos (destConst f) in 
-      mkConst (out_some finfos.equation_lemma)
-    with (Not_found | Failure "out_some" as e) -> 
+      mkConst (Option.get finfos.equation_lemma)
+    with (Not_found | Option.IsNone as e) -> 
       let f_id = id_of_label (con_label (destConst f)) in 
       (*i The next call to mk_equation_id is valid since we will construct the lemma
 	Ensures by: obvious
@@ -943,7 +943,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
       generate_equation_lemma all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num;
       let _ =
 	match e with 
-	  | Failure "out_some" -> 
+	  | Option.IsNone -> 
 	      let finfos = find_Function_infos (destConst f) in 
 	      update_Function 
 		{finfos with
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index cb804f6f2b..72f930b0a6 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -115,7 +115,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
     it_mkProd_or_LetIn 
       ~init:
       (it_mkProd_or_LetIn 
-	 ~init:(option_fold_right
+	 ~init:(Option.fold_right
 			   mkProd_or_LetIn
 			   princ_type_info.indarg
 			   princ_type_info.concl
@@ -564,9 +564,9 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent
   let opacity = 
     let finfos = find_Function_infos this_block_funs.(0) in 
     try 
-      let equation =  out_some finfos.equation_lemma in  
+      let equation =  Option.get finfos.equation_lemma in  
       (Global.lookup_constant equation).Declarations.const_opaque 
-    with Failure "out_some" -> (* non recursive definition *) 
+    with Option.IsNone -> (* non recursive definition *) 
       false
   in
   let const = {const with const_entry_opaque = opacity } in 
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 199e01525b..3102f1b5d7 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -48,8 +48,8 @@ let functional_induction with_clean c princl pat =
 			| InType -> finfo.rect_lemma
 		    in
 		    let princ =  (* then we get the principle *)
-		      try mkConst (out_some princ_option )
-		      with Failure "out_some" -> 
+		      try mkConst (Option.get princ_option )
+		      with Option.IsNone -> 
 			(*i If there is not default lemma defined then, 
 			  we cross our finger and try to find a lemma named f_ind 
 			  (or f_rec, f_rect) i*)
@@ -589,21 +589,21 @@ let rec add_args id new_args b =
       CApp(loc,(pf,add_args id new_args b), 
 	   List.map (fun (e,o) -> add_args id new_args e,o) bl)
   | CCases(loc,b_option,cel,cal) -> 
-      CCases(loc,option_map (add_args id new_args) b_option,
+      CCases(loc,Option.map (add_args id new_args) b_option,
 	     List.map (fun (b,(na,b_option)) -> 
 			 add_args id new_args b,
-			 (na,option_map (add_args id new_args) b_option)) cel, 
+			 (na,Option.map (add_args id new_args) b_option)) cel, 
 	     List.map (fun (loc,cpl,e) -> (loc,cpl,add_args id new_args e)) cal
 	    )
   | CLetTuple(loc,nal,(na,b_option),b1,b2) -> 
-      CLetTuple(loc,nal,(na,option_map (add_args id new_args) b_option),
+      CLetTuple(loc,nal,(na,Option.map (add_args id new_args) b_option),
 		add_args id new_args b1,
 		add_args id new_args b2
 	       )
 		
   | CIf(loc,b1,(na,b_option),b2,b3) -> 
       CIf(loc,add_args id new_args b1, 
-	  (na,option_map (add_args id new_args) b_option),
+	  (na,Option.map (add_args id new_args) b_option),
 	  add_args id new_args b2,
 	  add_args id new_args b3
 	 )
@@ -722,7 +722,7 @@ let make_graph (f_ref:global_reference) =
 			   )
 		       in 
 		       let rec_id = 
-			 match List.nth bl' (out_some n)  with 
+			 match List.nth bl' (Option.get n)  with 
 			   |(_,Name id) -> id | _ -> anomaly ""
 		       in
 		       let new_args = 
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index 609504ba5a..c2372d3ed0 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -319,12 +319,12 @@ let subst_Function (_,subst,finfos) =
   in
   let function_constant' = do_subst_con finfos.function_constant in 
   let graph_ind' = do_subst_ind finfos.graph_ind in 
-  let equation_lemma' = Util.option_smartmap do_subst_con finfos.equation_lemma in 
-  let correctness_lemma' = Util.option_smartmap do_subst_con finfos.correctness_lemma in 
-  let completeness_lemma' = Util.option_smartmap do_subst_con finfos.completeness_lemma in 
-  let rect_lemma' = Util.option_smartmap do_subst_con finfos.rect_lemma in
-  let rec_lemma' = Util.option_smartmap do_subst_con finfos.rec_lemma in 
-  let prop_lemma' =  Util.option_smartmap do_subst_con finfos.prop_lemma in 
+  let equation_lemma' = Option.smartmap do_subst_con finfos.equation_lemma in 
+  let correctness_lemma' = Option.smartmap do_subst_con finfos.correctness_lemma in 
+  let completeness_lemma' = Option.smartmap do_subst_con finfos.completeness_lemma in 
+  let rect_lemma' = Option.smartmap do_subst_con finfos.rect_lemma in
+  let rec_lemma' = Option.smartmap do_subst_con finfos.rec_lemma in 
+  let prop_lemma' =  Option.smartmap do_subst_con finfos.prop_lemma in 
   if function_constant' == finfos.function_constant && 
     graph_ind' == finfos.graph_ind && 
     equation_lemma' == finfos.equation_lemma &&
@@ -354,12 +354,12 @@ let export_Function infos = Some infos
 let discharge_Function (_,finfos) = 
   let function_constant' = Lib.discharge_con finfos.function_constant
   and graph_ind' = Lib.discharge_inductive finfos.graph_ind 
-  and equation_lemma' = Util.option_smartmap Lib.discharge_con finfos.equation_lemma 
-  and correctness_lemma' = Util.option_smartmap Lib.discharge_con finfos.correctness_lemma 
-  and completeness_lemma' = Util.option_smartmap Lib.discharge_con finfos.completeness_lemma 
-  and rect_lemma' = Util.option_smartmap Lib.discharge_con finfos.rect_lemma 
-  and rec_lemma' = Util.option_smartmap Lib.discharge_con finfos.rec_lemma
-  and prop_lemma' = Util.option_smartmap Lib.discharge_con finfos.prop_lemma
+  and equation_lemma' = Option.smartmap Lib.discharge_con finfos.equation_lemma 
+  and correctness_lemma' = Option.smartmap Lib.discharge_con finfos.correctness_lemma 
+  and completeness_lemma' = Option.smartmap Lib.discharge_con finfos.completeness_lemma 
+  and rect_lemma' = Option.smartmap Lib.discharge_con finfos.rect_lemma 
+  and rec_lemma' = Option.smartmap Lib.discharge_con finfos.rec_lemma
+  and prop_lemma' = Option.smartmap Lib.discharge_con finfos.prop_lemma
   in
   if function_constant' == finfos.function_constant && 
     graph_ind' == finfos.graph_ind && 
@@ -387,12 +387,12 @@ let pr_info f_info =
   str "function_constant := " ++ Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++
     str "function_constant_type := " ++ 
     (try Printer.pr_lconstr (Global.type_of_global (ConstRef f_info.function_constant)) with _ -> mt ()) ++ fnl () ++
-    str "equation_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.equation_lemma (mt ()) ) ++ fnl () ++
-    str "completeness_lemma :=" ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.completeness_lemma (mt ()) ) ++ fnl () ++
-    str "correctness_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.correctness_lemma (mt ()) ) ++ fnl () ++
-    str "rect_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rect_lemma (mt ()) ) ++ fnl () ++
-    str "rec_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rec_lemma (mt ()) ) ++ fnl () ++
-    str "prop_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.prop_lemma (mt ()) ) ++ fnl () ++
+    str "equation_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.equation_lemma (mt ()) ) ++ fnl () ++
+    str "completeness_lemma :=" ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.completeness_lemma (mt ()) ) ++ fnl () ++
+    str "correctness_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.correctness_lemma (mt ()) ) ++ fnl () ++
+    str "rect_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rect_lemma (mt ()) ) ++ fnl () ++
+    str "rec_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rec_lemma (mt ()) ) ++ fnl () ++
+    str "prop_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.prop_lemma (mt ()) ) ++ fnl () ++
     str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl () 
 
 let pr_table tb = 
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 6171e81948..dcbefe4a40 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -665,8 +665,8 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
       if infos.is_general ||  Rtree.is_infinite graph_def.mind_recargs
       then 
 	let eq_lemma = 
-	  try out_some (infos).equation_lemma
-	  with Failure "out_some"  -> anomaly "Cannot find equation lemma"
+	  try Option.get (infos).equation_lemma
+	  with Option.IsNone -> anomaly "Cannot find equation lemma"
 	in 
 	tclTHENSEQ[
 	  tclMAP h_intro ids;
@@ -769,7 +769,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	  Array.of_list 
 	    (List.map 
 	       (fun entry -> 
-		  (entry.Entries.const_entry_body, out_some entry.Entries.const_entry_type )
+		  (entry.Entries.const_entry_body, Option.get entry.Entries.const_entry_type )
 	       )
 	       (make_scheme (array_map_to_list (fun const -> const,Rawterm.RType None) funs))
 	    )
@@ -960,13 +960,13 @@ let invfun qhyp f  =
   in
   try 
     let finfos = find_Function_infos f in 
-    let f_correct = mkConst(out_some finfos.correctness_lemma) 
+    let f_correct = mkConst(Option.get finfos.correctness_lemma) 
     and kn = fst finfos.graph_ind
     in
     Tactics.try_intros_until (fun hid -> functional_inversion kn hid (mkConst f)  f_correct) qhyp 
   with 
     | Not_found ->  error "No graph found" 
-    | Failure "out_some"  -> error "Cannot use equivalence with graph!"
+    | Option.IsNone  -> error "Cannot use equivalence with graph!"
 
 
 let invfun qhyp f g = 
@@ -983,23 +983,23 @@ let invfun qhyp f g =
 		     try 
 		       if not (isConst f1) then failwith "";
 		       let finfos = find_Function_infos (destConst f1) in 
-		       let f_correct = mkConst(out_some finfos.correctness_lemma) 
+		       let f_correct = mkConst(Option.get finfos.correctness_lemma) 
 		       and kn = fst finfos.graph_ind
 		       in
 		       functional_inversion kn hid f1 f_correct g
-		     with | Failure "" | Failure "out_some" | Not_found -> 
+		     with | Failure "" | Option.IsNone | Not_found -> 
 		       try 
 			 let f2,_ = decompose_app args.(2) in 
 			 if not (isConst f2) then failwith "";
 			 let finfos = find_Function_infos (destConst f2) in 
-			 let f_correct = mkConst(out_some finfos.correctness_lemma) 
+			 let f_correct = mkConst(Option.get finfos.correctness_lemma) 
 			 and kn = fst finfos.graph_ind
 			 in
 			 functional_inversion kn hid  f2 f_correct g
 		       with
 			 | Failure "" -> 
 			     errorlabstrm "" (str "Hypothesis" ++ Ppconstr.pr_id hid ++ str " must contain at leat one Function")
-			 | Failure "out_some"  ->  
+			 | Option.IsNone  ->  
 			     if do_observe () 
 			     then
 			       error "Cannot use equivalence with graph for any side of the equality"
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index b34a1097a3..af0a2addc8 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -368,7 +368,7 @@ let raw_push_named (na,raw_value,raw_typ) env =
   match na with 
     | Anonymous -> env 
     | Name id -> 
-	let value = Util.option_map (Pretyping.Default.understand Evd.empty env) raw_value in 
+	let value = Option.map (Pretyping.Default.understand Evd.empty env) raw_value in 
 	let typ = Pretyping.Default.understand_type Evd.empty env raw_typ in 
 	Environ.push_named (id,value,typ) env
 
@@ -398,12 +398,12 @@ let add_pat_variables pat typ env : Environ.env =
 	   | Anonymous -> assert false
 	   | Name id ->
 	       let new_t =  substl ctxt t in
-	       let new_v = option_map (substl ctxt) v in
+	       let new_v = Option.map (substl ctxt) v in
 	       observe (str "for variable " ++ Ppconstr.pr_id id ++  fnl () ++
 			  str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++
 			  str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++
-			  option_fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++
-			  option_fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ())
+			  Option.fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++
+			  Option.fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ())
 		       );
 	       (Environ.push_named (id,new_v,new_t) env,mkVar id::ctxt)
       )
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index f9e188dacf..e8cce47adb 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -157,7 +157,7 @@ let change_vars =
 	  let new_mapping = List.fold_left remove_name_from_mapping mapping nal in 
 	  RLetTuple(loc,
 		    nal,
-		    (na, option_map (change_vars mapping) rto), 
+		    (na, Option.map (change_vars mapping) rto), 
 		    change_vars mapping b, 
 		    change_vars new_mapping e
 		   )
@@ -170,7 +170,7 @@ let change_vars =
       | RIf(loc,b,(na,e_option),lhs,rhs) -> 
 	  RIf(loc,
 	      change_vars mapping b,
-	      (na,option_map (change_vars mapping) e_option),
+	      (na,Option.map (change_vars mapping) e_option),
 	      change_vars mapping lhs,
 	      change_vars mapping rhs
 	     )
@@ -338,11 +338,11 @@ let rec alpha_rt excluded rt =
 	  if idmap_is_empty mapping
 	  then rto,t,b
 	  else let replace = change_vars mapping in 
-	  (option_map replace rto, t,replace b)
+	  (Option.map replace rto, t,replace b)
 	in
 	let new_t = alpha_rt new_excluded new_t in 
 	let new_b = alpha_rt new_excluded new_b in 
-	let new_rto = option_map (alpha_rt new_excluded) new_rto  in
+	let new_rto = Option.map (alpha_rt new_excluded) new_rto  in
 	RLetTuple(loc,new_nal,(na,new_rto),new_t,new_b)
     | RCases(loc,infos,el,brl) -> 
 	let new_el = 
@@ -351,7 +351,7 @@ let rec alpha_rt excluded rt =
 	RCases(loc,infos,new_el,List.map (alpha_br excluded) brl) 
     | RIf(loc,b,(na,e_o),lhs,rhs) -> 
 	RIf(loc,alpha_rt excluded b,
-	    (na,option_map (alpha_rt excluded) e_o),
+	    (na,Option.map (alpha_rt excluded) e_o),
 	    alpha_rt excluded lhs,
 	    alpha_rt excluded rhs
 	   )
@@ -487,7 +487,7 @@ let replace_var_by_term x_id term =
       | RLetTuple(loc,nal,(na,rto),def,b) -> 
 	  RLetTuple(loc,
 		    nal,
-		    (na,option_map replace_var_by_pattern rto),
+		    (na,Option.map replace_var_by_pattern rto),
 		    replace_var_by_pattern def,
 		    replace_var_by_pattern b
 		   )
@@ -499,7 +499,7 @@ let replace_var_by_term x_id term =
 		)
       | RIf(loc,b,(na,e_option),lhs,rhs) -> 
 	  RIf(loc, replace_var_by_pattern b,
-	      (na,option_map replace_var_by_pattern e_option),
+	      (na,Option.map replace_var_by_pattern e_option),
 	      replace_var_by_pattern lhs,
 	      replace_var_by_pattern rhs
 	     )
@@ -640,7 +640,7 @@ let zeta_normalize =
       | RLetTuple(loc,nal,(na,rto),def,b) -> 
 	  RLetTuple(loc,
 		    nal,
-		    (na,option_map zeta_normalize_term rto),
+		    (na,Option.map zeta_normalize_term rto),
 		    zeta_normalize_term def,
 		    zeta_normalize_term b
 		   )
@@ -652,7 +652,7 @@ let zeta_normalize =
 		)
       | RIf(loc,b,(na,e_option),lhs,rhs) -> 
 	  RIf(loc, zeta_normalize_term b,
-	      (na,option_map zeta_normalize_term e_option),
+	      (na,Option.map zeta_normalize_term e_option),
 	      zeta_normalize_term lhs,
 	      zeta_normalize_term rhs
 	     )
@@ -695,17 +695,17 @@ let expand_as =
       | RProd(loc,na,t,b) -> RProd(loc,na,expand_as map t, expand_as map b)
       | RLetIn(loc,na,v,b) -> RLetIn(loc,na, expand_as map v,expand_as map b)
       | RLetTuple(loc,nal,(na,po),v,b) ->
-	  RLetTuple(loc,nal,(na,option_map (expand_as map) po),
+	  RLetTuple(loc,nal,(na,Option.map (expand_as map) po),
 		    expand_as map v, expand_as map b)
       | RIf(loc,e,(na,po),br1,br2) ->
-	  RIf(loc,expand_as map e,(na,option_map (expand_as map) po),
+	  RIf(loc,expand_as map e,(na,Option.map (expand_as map) po),
 	      expand_as map br1, expand_as map br2)
       | RRec _ ->  error "Not handled RRec"
       | RDynamic _ -> error "Not handled RDynamic"
       | RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t))
       | RCast(loc,b,CastCoerce) -> RCast(loc,expand_as map b,CastCoerce)
       | RCases(loc,po,el,brl) ->
-	  RCases(loc, option_map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
+	  RCases(loc, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
 		List.map (expand_as_br map) brl)
 	    
   and expand_as_br map (loc,idl,cpl,rt) =