parameter sintax added to axiom statement

[helm.git] / helm / software / components / cic / deannotate.mli

diff --git a/helm/software/components/cic/deannotate.mli b/helm/software/components/cic/deannotate.mli
index 89b18d2d6faca057879068950560fed48f5df0a8..f4fdd2d5d59e918a53217323cd79c2f397417a9c 100644 (file)
--- a/helm/software/components/cic/deannotate.mli
+++ b/helm/software/components/cic/deannotate.mli
@@ -32,5 +32,9 @@
 (*                                                                            *)
 (******************************************************************************)
 
+val type_of_aux' : (Cic.context -> Cic.term -> Cic.term) ref
+val lift : (int -> Cic.term -> Cic.term) ref
+
 val deannotate_term : Cic.annterm -> Cic.term
+val deannotate_conjectures : Cic.annmetasenv -> Cic.metasenv
 val deannotate_obj : Cic.annobj -> Cic.obj