]> matita.cs.unibo.it Git - helm.git/commitdiff
added type to explicit substitutions
authorAndrea Asperti <andrea.asperti@unibo.it>
Fri, 22 Oct 2004 11:54:57 +0000 (11:54 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Fri, 22 Oct 2004 11:54:57 +0000 (11:54 +0000)
helm/ocaml/cic/cic.ml

index 7dc86114d7e72d82eff94fbde167a9576deaeca2..c997d99ca3d3a866fbed691f1929803f46149b8c 100644 (file)
@@ -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