From 38633ee024797543bba347addb8f287fd3e5331f Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 29 Nov 2004 12:20:06 +0000 Subject: [PATCH] bugfix in type_of_aux' which erroneously discard given substitution (fixes a lot of CicUtil.Meta_not_found spurious exceptions) --- helm/ocaml/cic_proof_checking/cicTypeChecker.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.39.2