Procedural: 2 bug fix in eta expansion + 1 bug fix in pattern generation

[helm.git] / components / acic_procedural / proceduralConversion.mli

diff --git a/components/acic_procedural/proceduralConversion.mli b/components/acic_procedural/proceduralConversion.mli
index d5ad4fd1c9634e7620bc4f8d9f53195792ceeeb4..3b65200144a1e9f40eee72bf0a094fdb9d76d39d 100644 (file)
--- a/components/acic_procedural/proceduralConversion.mli
+++ b/components/acic_procedural/proceduralConversion.mli
@@ -23,6 +23,11 @@
  * http://cs.unibo.it/helm/.
  *)
 
-val need_whd: int -> Cic.annterm -> bool
-
 val lift: int -> int -> Cic.annterm -> Cic.annterm
+
+val mk_ind: 
+   Cic.context -> Cic.id -> UriManager.uri -> int -> 
+   Cic.annterm -> Cic.annterm -> Cic.annterm list ->
+   Cic.annterm option
+
+val mk_pattern: Cic.annterm list -> Cic.annterm -> Cic.annterm