X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic%2Fcic.ml;h=c997d99ca3d3a866fbed691f1929803f46149b8c;hb=afd3b379d4959e4a18c1f26f25e4a9c14997866f;hp=7dc86114d7e72d82eff94fbde167a9576deaeca2;hpb=4767ed3aba79ed1d06c6d4e2d195b77e5bd26db5;p=helm.git

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index 7dc86114d..c997d99ca 100644
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -110,7 +110,7 @@ and coInductiveFun =
 (* depend on new ones.                                           *)
 and conjecture = int * context * term
 and metasenv = conjecture list
-and substitution = (int * (context * term)) list
+and substitution = (int * (context * term * term)) list