ancient graph regarding universes and trust=false, universes calculated for internal...

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 4a78e324a687b0b2b651892144b5272372c590b0..bcdb340bd1d137af0393fbd1cf2cfe6fc028fc17 100644 (file)
--- 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
 ;;