From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 29 Nov 2004 12:20:06 +0000 (+0000)
Subject: bugfix in type_of_aux' which erroneously discard given substitution
X-Git-Tag: PRE_UNIVERSES~9
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=38633ee024797543bba347addb8f287fd3e5331f;p=helm.git

bugfix in type_of_aux' which erroneously discard given substitution
(fixes a lot of CicUtil.Meta_not_found spurious exceptions)
---

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index e4dbee6ef..be7c4b0d0 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1863,7 +1863,7 @@ let typecheck uri =
 
 let type_of_aux' ?(subst = []) metasenv context t =
   let logger = new CicLogger.logger in
-  type_of_aux' ~logger metasenv context t
+  type_of_aux' ~logger ~subst metasenv context t
 
 let typecheck_mutual_inductive_defs uri (itl, uris, indparamsno) =
   let logger = new CicLogger.logger in