From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 3 Oct 2005 08:16:07 +0000 (+0000)
Subject: the filled object is inserted in the env after a successful typechecking
X-Git-Tag: V_0_7_2_3~263
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=74b79a859c4bdfbc82d6bb05bb9b28501082bbc7;p=helm.git

the filled object is inserted in the env after a successful typechecking
---

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 *)