X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=1577b2f3f64b8b85ed7c2378635c2a5d6ab50f74;hb=6c3a5a7adc3f37ddfb99a69b050fbf324e95e583;hp=140e4171287a73a4b1164f857306f31368bb2806;hpb=655906d74521fa49de332f54ec34bfc9d9744151;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 140e41712..1577b2f3f 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1390,7 +1390,8 @@ and type_of_aux' metasenv context t =
     | C.Prod (name,s,t) ->
        let sort1 = type_of_aux context s
        and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
-        sort_of_prod context (name,s) (sort1,sort2)
+       let res = sort_of_prod context (name,s) (sort1,sort2) in
+      res
    | C.Lambda (n,s,t) ->
        let sort1 = type_of_aux context s in
        (match R.whd context sort1 with
@@ -1423,8 +1424,8 @@ and type_of_aux' metasenv context t =
        (CicSubstitution.subst s
         (type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t))
    | C.Appl (he::tl) when List.length tl > 0 ->
-      let hetype = type_of_aux context he
-      and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
+      let hetype = type_of_aux context he in
+      let tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
        eat_prods context hetype tlbody_and_type
    | C.Appl _ -> raise (AssertFailure "Appl: no arguments")
    | C.Const (uri,exp_named_subst) ->
@@ -1636,6 +1637,7 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^
     | ((uri,t) as subst)::tl ->
        let typeofvar =
         CicSubstitution.subst_vars substs (type_of_variable uri) in
+(* CSC: this test should not exist
        (match CicEnvironment.get_cooked_obj ~trust:false uri with
            Cic.Variable (_,Some bo,_,_) ->
             raise
@@ -1647,6 +1649,7 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^
               ("Unknown variable definition:" ^
               UriManager.string_of_uri uri))
        ) ;
+*)
        let typeoft = type_of_aux context t in
         if CicReduction.are_convertible context typeoft typeofvar then
          check_exp_named_subst_aux (substs@[subst]) tl