From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 22 Oct 2004 11:54:57 +0000 (+0000)
Subject: added type to explicit substitutions
X-Git-Tag: V_0_0_10~51
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=125388497f1e123ac90e9b1167c99f41751eab90;p=helm.git

added type to explicit substitutions
---

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