added type to explicit substitutions

[helm.git] / helm / ocaml / cic / cic.ml

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index 7dc86114d7e72d82eff94fbde167a9576deaeca2..c997d99ca3d3a866fbed691f1929803f46149b8c 100644 (file)
--- 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