From 74b79a859c4bdfbc82d6bb05bb9b28501082bbc7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 3 Oct 2005 08:16:07 +0000 Subject: [PATCH] the filled object is inserted in the env after a successful typechecking --- 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 ee7638906..18de8af5e 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -2148,7 +2148,7 @@ let typecheck uri = let typecheck_obj ~logger uri obj = let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in - let ugraph, univlist = CicUnivUtils.clean_and_fill uri obj ugraph in + let ugraph, univlist, obj = CicUnivUtils.clean_and_fill uri obj ugraph in CicEnvironment.add_type_checked_obj uri (obj,ugraph,univlist) (** wrappers which instantiate fresh loggers *) -- 2.39.2