From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 19 Apr 2008 16:30:21 +0000 (+0000)
Subject: ancient graph regarding universes and trust=false, universes calculated for internal... 
X-Git-Tag: make_still_working~5311
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e8f4be1c4c7d4162035dd45ac4ea38b9ed168098;p=helm.git

ancient graph regarding universes and trust=false, universes calculated for internal objects
were used for the toplevel object (that should be sound) but cleaned using the univ list of
the internal object
---

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 4a78e324a..bcdb340bd 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -66,7 +66,7 @@ let check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri obj =
      else 
       ug,ul,obj
  | None -> 
-     CicUnivUtils.clean_and_fill uri obj inferred_ugraph
+     CicUnivUtils.clean_and_fill uri obj inferred_ugraph 
 ;;
 
 let debrujin_constructor ?(cb=fun _ _ -> ()) ?(check_exp_named_subst=true) uri number_of_types context =
@@ -141,7 +141,7 @@ let debrujin_constructor ?(cb=fun _ _ -> ()) ?(check_exp_named_subst=true) uri n
 
 exception CicEnvironmentError;;
 
-let rec type_of_constant ~logger uri ugraph =
+let rec type_of_constant ~logger uri (ugraph as orig_ugraph) =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
@@ -195,7 +195,7 @@ let rec type_of_constant ~logger uri ugraph =
        let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
        CicEnvironment.set_type_checking_info uri (obj, ugraph, ul);
        logger#log (`Type_checking_completed uri) ;
-       match CicEnvironment.is_type_checked ~trust:false ugraph uri with
+       match CicEnvironment.is_type_checked ~trust:false orig_ugraph uri with
            CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
          | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
   in
@@ -205,7 +205,7 @@ let rec type_of_constant ~logger uri ugraph =
     | _ ->
         raise (TypeCheckerFailure (lazy ("Unknown constant:" ^ U.string_of_uri uri)))
 
-and type_of_variable ~logger uri ugraph =
+and type_of_variable ~logger uri (ugraph as orig_ugraph) =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
@@ -231,7 +231,7 @@ and type_of_variable ~logger uri ugraph =
        let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
        CicEnvironment.set_type_checking_info uri (obj, ugraph, ul);
        logger#log (`Type_checking_completed uri) ;
-       (match CicEnvironment.is_type_checked ~trust:false ugraph uri with
+       (match CicEnvironment.is_type_checked ~trust:false orig_ugraph uri with
            CicEnvironment.CheckedObj((C.Variable(_,_,ty,_,_)),ugraph)->ty,ugraph
          | CicEnvironment.CheckedObj _ 
          | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError)
@@ -595,7 +595,7 @@ and check_mutual_inductive_defs uri obj ugraph =
 		lazy ("Unknown mutual inductive definition:" ^
 		 UriManager.string_of_uri uri)))
 
-and type_of_mutual_inductive_defs ~logger uri i ugraph =
+and type_of_mutual_inductive_defs ~logger uri i (ugraph as orig_ugraph) =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
@@ -608,7 +608,7 @@ and type_of_mutual_inductive_defs ~logger uri i ugraph =
          let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
 	 CicEnvironment.set_type_checking_info uri (obj,ugraph,ul);
 	 logger#log (`Type_checking_completed uri) ;
-	 (match CicEnvironment.is_type_checked ~trust:false ugraph uri with
+	 (match CicEnvironment.is_type_checked ~trust:false orig_ugraph uri with
 	      CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph')
 	    | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
 	 )
@@ -621,7 +621,7 @@ and type_of_mutual_inductive_defs ~logger uri i ugraph =
 	  raise (TypeCheckerFailure
            (lazy ("Unknown mutual inductive definition:" ^ U.string_of_uri uri)))
 	    
-and type_of_mutual_inductive_constr ~logger uri i j ugraph =
+and type_of_mutual_inductive_constr ~logger uri i j (ugraph as orig_ugraph) =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
@@ -637,7 +637,7 @@ and type_of_mutual_inductive_constr ~logger uri i j ugraph =
 	  CicEnvironment.set_type_checking_info uri (obj, ugraph, ul);
 	  logger#log (`Type_checking_completed uri) ;
 	  (match 
-             CicEnvironment.is_type_checked ~trust:false ugraph uri 
+             CicEnvironment.is_type_checked ~trust:false orig_ugraph uri 
            with
 		 CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' 
 	       | CicEnvironment.UncheckedObj _ -> 
@@ -2118,7 +2118,7 @@ let typecheck uri =
       let ugraph, ul, obj = typecheck_obj0 ~logger uri (uobj,unchecked_ugraph) in
       CicEnvironment.set_type_checking_info uri (obj,ugraph,ul);
       logger#log (`Type_checking_completed uri);
-      match CicEnvironment.is_type_checked ~trust:false ugraph uri with
+      match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with
       | CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
       | _ -> raise CicEnvironmentError
 ;;