Porting to the new metadata DTD.

[helm.git] / helm / ocaml / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 57bc5e2ad3698be43ae6a93e77d45b0273d100bb..7e96de2a42aca82b8acdc7e7d57ebba1d949840a 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -124,7 +124,7 @@ let rec type_of_constant uri =
  let module R = CicReduction in
  let module U = UriManager in
   let cobj =
-   match CicEnvironment.is_type_checked uri with
+   match CicEnvironment.is_type_checked ~trust:true uri with
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        Logger.log (`Start_type_checking uri) ;
@@ -153,7 +153,7 @@ let rec type_of_constant uri =
        ) ;
        CicEnvironment.set_type_checking_info uri ;
        Logger.log (`Type_checking_completed uri) ;
-       match CicEnvironment.is_type_checked uri with
+       match CicEnvironment.is_type_checked ~trust:false uri with
           CicEnvironment.CheckedObj cobj -> cobj
         | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
   in
@@ -167,7 +167,7 @@ and type_of_variable uri =
  let module R = CicReduction in
  let module U = UriManager in
   (* 0 because a variable is never cooked => no partial cooking at one level *)
-  match CicEnvironment.is_type_checked uri with
+  match CicEnvironment.is_type_checked ~trust:true uri with
      CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty
    | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) ->
       Logger.log (`Start_type_checking uri) ;
@@ -477,14 +477,14 @@ and type_of_mutual_inductive_defs uri i =
  let module R = CicReduction in
  let module U = UriManager in
   let cobj =
-   match CicEnvironment.is_type_checked uri with
+   match CicEnvironment.is_type_checked ~trust:true uri with
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        Logger.log (`Start_type_checking uri) ;
        check_mutual_inductive_defs uri uobj ;
        CicEnvironment.set_type_checking_info uri ;
        Logger.log (`Type_checking_completed uri) ;
-       (match CicEnvironment.is_type_checked uri with
+       (match CicEnvironment.is_type_checked ~trust:false uri with
           CicEnvironment.CheckedObj cobj -> cobj
         | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
        )
@@ -500,14 +500,14 @@ and type_of_mutual_inductive_constr uri i j =
  let module R = CicReduction in
  let module U = UriManager in
   let cobj =
-   match CicEnvironment.is_type_checked uri with
+   match CicEnvironment.is_type_checked ~trust:true uri with
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        Logger.log (`Start_type_checking uri) ;
        check_mutual_inductive_defs uri uobj ;
        CicEnvironment.set_type_checking_info uri ;
        Logger.log (`Type_checking_completed uri) ;
-       (match CicEnvironment.is_type_checked uri with
+       (match CicEnvironment.is_type_checked ~trust:false uri with
           CicEnvironment.CheckedObj cobj -> cobj
         | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
        )
@@ -934,7 +934,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
        List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
    | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
       let consty =
-       match CicEnvironment.get_cooked_obj uri with
+       match CicEnvironment.get_cooked_obj ~trust:false uri with
           C.InductiveDefinition (itl,_,_) ->
            let (_,_,_,cl) = List.nth itl i in
             let (_,cons) = List.nth cl (j - 1) in
@@ -1393,7 +1393,7 @@ and type_of_aux' metasenv context t =
 
         (* let's check if the type of branches are right *)
         let parsno =
-         match CicEnvironment.get_cooked_obj uri with
+         match CicEnvironment.get_cooked_obj ~trust:false uri with
             C.InductiveDefinition (_,_,parsno) -> parsno
           | _ ->
             raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
@@ -1504,7 +1504,7 @@ in if not res then prerr_endline ("#### " ^ CicPp.ppterm (type_of_aux context p)
     | ((uri,t) as subst)::tl ->
        let typeofvar =
         CicSubstitution.subst_vars substs (type_of_variable uri) in
-       (match CicEnvironment.get_cooked_obj uri with
+       (match CicEnvironment.get_cooked_obj ~trust:false uri with
            Cic.Variable (_,Some bo,_,_) ->
             raise
              (NotWellTyped
@@ -1568,7 +1568,7 @@ in if not res then prerr_endline ("#### " ^ CicPp.ppterm (type_of_aux context p)
    match CicReduction.whd context ty with
       C.MutInd (uri,i,_) ->
        (*CSC: definire una funzioncina per questo codice sempre replicato *)
-       (match CicEnvironment.get_cooked_obj uri with
+       (match CicEnvironment.get_cooked_obj ~trust:false uri with
            C.InductiveDefinition (itl,_,_) ->
             let (_,is_inductive,_,_) = List.nth itl i in
              if is_inductive then None else (Some uri)
@@ -1630,7 +1630,7 @@ let typecheck uri =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
-  match CicEnvironment.is_type_checked uri with
+  match CicEnvironment.is_type_checked ~trust:false uri with
      CicEnvironment.CheckedObj _ -> ()
    | CicEnvironment.UncheckedObj uobj ->
       (* let's typecheck the uncooked object *)