Splitting out of auto.ml a file hints.ml dedicated to hints so as to

being able to export hints without tactics, vm, etc. to come with.

Some functions moved to the new proof engine.

2 files changed, 12 insertions, 0 deletions

diff --git a/lib/cList.ml b/lib/cList.ml
index 93ba0637e..3115826c6 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -61,6 +61,7 @@ sig
   val except : 'a eq -> 'a -> 'a list -> 'a list
   val remove : 'a eq -> 'a -> 'a list -> 'a list
   val remove_first : ('a -> bool) -> 'a list -> 'a list
+  val insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
   val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
   val sep_last : 'a list -> 'a * 'a list
   val find_map : ('a -> 'b option) -> 'a list -> 'b
@@ -442,6 +443,13 @@ let rec remove_first p = function
   | b::l -> b::remove_first p l
   | [] -> raise Not_found
 
+let insert p v l =
+  let rec insrec = function
+    | [] -> [v]
+    | h::tl -> if p v h then v::h::tl else h::insrec tl
+  in
+  insrec l
+
 let add_set cmp x l = if mem_f cmp x l then l else x :: l
 
 (** List equality up to permutation (but considering multiple occurrences) *)
diff --git a/lib/cList.mli b/lib/cList.mli
index 01ae83960..aa888679c 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -119,6 +119,10 @@ sig
   val remove_first : ('a -> bool) -> 'a list -> 'a list
   (** Remove the first element satisfying a predicate, or raise [Not_found] *)
 
+  val insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
+  (** Insert at the (first) position so that if the list is ordered wrt to the
+      total order given as argument, the order is preserved *)
+
   val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
   val sep_last : 'a list -> 'a * 'a list