From e3e2bec0f31390fe797d65961a14f7cd78bc4109 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 19 Jul 2019 03:41:07 +0200
Subject: [funind] Port indfun to the new tactic engine.

---
 plugins/funind/indfun_common.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins/funind/indfun_common.mli')

diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index fff4711044..0815ca882a 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -38,7 +38,6 @@ val chop_rprod_n : int -> Glob_term.glob_constr ->
 
 val eq : EConstr.constr Lazy.t
 val refl_equal : EConstr.constr Lazy.t
-val const_of_id: Id.t ->  GlobRef.t(* constantyes *)
 val jmeq : unit -> EConstr.constr
 val jmeq_refl : unit -> EConstr.constr
 val make_eq : unit -> EConstr.constr
-- 
cgit v1.2.3


From 1f972321c232b8e2445008af763fcae4ac4ea946 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 7 Aug 2019 20:02:43 +0200
Subject: [funind] Move some exception-based control flow to explicit option
 typing.

---
 plugins/funind/indfun_common.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/funind/indfun_common.mli')

diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 0815ca882a..16beaaa3c7 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -74,8 +74,8 @@ type function_info =
       is_general : bool;
     }
 
-val find_Function_infos : Constant.t -> function_info
-val find_Function_of_graph : inductive -> function_info
+val find_Function_infos : Constant.t -> function_info option
+val find_Function_of_graph : inductive -> function_info option
 (* WARNING: To be used just after the graph definition !!! *)
 val add_Function : bool -> Constant.t -> unit
 val update_Function : function_info -> unit
-- 
cgit v1.2.3