bugfix in type_of_aux' which erroneously discard given substitution

[helm.git] / helm / ocaml / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index e4dbee6ef96e8ed1870a37010bd2ca74f08d345d..be7c4b0d0aeaca45b0dc26704bf92a3dde6032c5 100644 (file)
--- 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