aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/nsatz/utile.mli
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-03-13 00:00:12 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-03-13 00:00:12 +0000
commit552df1605233769ad3cdabaadaa0011605e79797 (patch)
tree28c3ae6a250aba80e1eb53ff9d906df9f49b75c1 /plugins/nsatz/utile.mli
parentda3cbbcef1f4de9780603225e095f026bb5da709 (diff)
Restrict (try...with...) to avoid catching critical exn (part 7)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16283 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/nsatz/utile.mli')
-rw-r--r--plugins/nsatz/utile.mli4
1 files changed, 0 insertions, 4 deletions
diff --git a/plugins/nsatz/utile.mli b/plugins/nsatz/utile.mli
index 83b2ac39b..1f8415752 100644
--- a/plugins/nsatz/utile.mli
+++ b/plugins/nsatz/utile.mli
@@ -10,10 +10,6 @@ val info : string -> unit
val list_mem_eq : ('a -> 'b -> bool) -> 'a -> 'b list -> bool
val set_of_list_eq : ('a -> 'a -> bool) -> 'a list -> 'a list
-(* Memoization *)
-val memos :
- string -> ('a, 'b) Hashtbl.t -> ('c -> 'a) -> ('c -> 'b) -> 'c -> 'b
-
val facteurs_liste : ('a -> 'a -> 'a) -> ('a -> bool) -> 'a list -> 'a list
val factorise_tableau :