content2Procedural.ml: "Intros+LetTac" ok

[helm.git] / helm / software / components / content_pres / content2Procedural.mli

diff --git a/helm/software/components/content_pres/content2Procedural.mli b/helm/software/components/content_pres/content2Procedural.mli
index 06123000e21755132aaf2849a1213ee478496e60..938d4dd6b1f1a0c4ccf30f71369d317182b8f9bf 100644 (file)
--- a/helm/software/components/content_pres/content2Procedural.mli
+++ b/helm/software/components/content_pres/content2Procedural.mli
@@ -26,7 +26,7 @@
 val content2procedural:
    ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> string ->
    Cic.annterm Content.cobj ->
-      (CicNotationPt.term, CicNotationPt.term,
-       CicNotationPt.term GrafiteAst.reduction, CicNotationPt.term CicNotationPt.obj, string)
+      (Cic.annterm, Cic.annterm,
+       Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string)
       GrafiteAst.statement list