X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2Fdeannotate.mli;h=f4fdd2d5d59e918a53217323cd79c2f397417a9c;hb=HEAD;hp=89b18d2d6faca057879068950560fed48f5df0a8;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/cic/deannotate.mli b/helm/software/components/cic/deannotate.mli
index 89b18d2d6..f4fdd2d5d 100644
--- 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