diff options
| -rw-r--r-- | ide/coqide.ml | 3 | ||||
| -rw-r--r-- | interp/topconstr.ml | 2 | ||||
| -rw-r--r-- | lib/option.ml | 11 | ||||
| -rw-r--r-- | lib/option.mli | 7 | ||||
| -rw-r--r-- | lib/util.ml | 5 | ||||
| -rw-r--r-- | lib/util.mli | 3 | ||||
| -rw-r--r-- | library/declaremods.ml | 2 |
7 files changed, 20 insertions, 13 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index cda306eb2..9860870ca 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -13,9 +13,6 @@ open Vernacexpr open Coq open Ideutils -let Option.get s = match s with - | None -> failwith "Internal error in Option.get" | Some f -> f - let cb_ = ref None let cb () = ((Option.get !cb_):GData.clipboard) let last_cb_content = ref "" diff --git a/interp/topconstr.ml b/interp/topconstr.ml index fcf383937..e29f17210 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -451,7 +451,7 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with & List.length eqnl1 = List.length eqnl2 -> let rtno1' = abstract_return_type_context_rawconstr tml1 rtno1 in let rtno2' = abstract_return_type_context_aconstr tml2 rtno2 in - let sigma = option_fold_left2 (match_ alp metas) sigma rtno1' rtno2' in + let sigma = Option.fold_left2 (match_ alp metas) sigma rtno1' rtno2' in let sigma = List.fold_left2 (fun s (tm1,_) (tm2,_) -> match_ alp metas s tm1 tm2) sigma tml1 tml2 in List.fold_left2 (match_equations alp metas) sigma eqnl1 eqnl2 diff --git a/lib/option.ml b/lib/option.ml index 96b9c70e8..0ed36b002 100644 --- a/lib/option.ml +++ b/lib/option.ml @@ -29,6 +29,8 @@ let get = function | Some y -> y | _ -> raise IsNone +(** [make x] returns [Some x]. *) +let make x = Some x (** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *) let flatten = function @@ -72,6 +74,15 @@ let fold_left f a = function | Some y -> f a y | _ -> a +(** [fold_left2 f a x y] is [f z w] if [x] is [Some z] and [y] is [Some w]. + It is [a] if both [x] and [y] are [None]. Otherwise it raises + [Heterogeneous]. *) +let fold_left2 f a x y = + match x,y with + | Some x, Some y -> f a x y + | None, None -> a + | _ -> raise Heterogeneous + (** [fold_right f x a] is [f y a] if [x] is [Some y], and [a] otherwise. *) let fold_right f x a = match x with diff --git a/lib/option.mli b/lib/option.mli index 0a22697e7..f98c45ee7 100644 --- a/lib/option.mli +++ b/lib/option.mli @@ -25,6 +25,8 @@ exception IsNone if [x] equals [None]. *) val get : 'a option -> 'a +(** [make x] returns [Some x]. *) +val make : 'a -> 'a option (** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *) val flatten : 'a option option -> 'a option @@ -53,6 +55,11 @@ val smartmap : ('a -> 'a) -> 'a option -> 'a option (** [fold_left f a x] is [f a y] if [x] is [Some y], and [a] otherwise. *) val fold_left : ('b -> 'a -> 'b) -> 'b -> 'a option -> 'b +(** [fold_left2 f a x y] is [f z w] if [x] is [Some z] and [y] is [Some w]. + It is [a] if both [x] and [y] are [None]. Otherwise it raises + [Heterogeneous]. *) +val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option -> 'c option -> 'a + (** [fold_right f x a] is [f y a] if [x] is [Some y], and [a] otherwise. *) val fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b diff --git a/lib/util.ml b/lib/util.ml index 389d0e129..b61cd88ff 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -788,15 +788,10 @@ let interval n m = in interval_n ([],m) -let in_some x = Some x - let option_cons a l = match a with | Some x -> x::l | None -> l -let option_fold_left2 f e a b = match (a,b) with - | Some x, Some y -> f e x y - let option_compare f a b = match (a,b) with | None, None -> true | Some a', Some b' -> f a' b' diff --git a/lib/util.mli b/lib/util.mli index 0282f45f5..71262bb4c 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -223,10 +223,7 @@ val intmap_inv : 'a Intmap.t -> 'a -> int list val interval : int -> int -> int list -val in_some : 'a -> 'a option val option_cons : 'a option -> 'a list -> 'a list -val option_fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option -> - 'c option -> 'a val option_compare : ('a -> 'b -> bool) -> 'a option -> 'b option -> bool val filter_some : 'a option list -> 'a list diff --git a/library/declaremods.ml b/library/declaremods.ml index 6a73943b9..29e8012fe 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -381,7 +381,7 @@ let (in_modtype,out_modtype) = load_function = load_modtype; subst_function = subst_modtype; classify_function = classify_modtype; - export_function = in_some } + export_function = Option.make } |