Just code clean-up.

[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 f33d56e1b9ceedbe061db7cc7562046f7ab5b3e4..77a1251605f2915e0fa6c8a9cc349d5feec86461 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1019,9 +1019,7 @@ and type_of_aux' env t =
    | C.Appl (he::tl) when List.length tl > 0 ->
       let hetype = type_of_aux env he
       and tlbody_and_type = List.map (fun x -> (x, type_of_aux env x)) tl in
-       (try
-        eat_prods hetype tlbody_and_type
-       with _ -> debug (C.Appl (he::tl)) env ; C.Implicit)
+       eat_prods hetype tlbody_and_type
    | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
    | C.Const (uri,cookingsno) ->
       incr fdebug ;
@@ -1196,15 +1194,16 @@ and type_of_aux' env t =
         Cic.Prod (n,s,t) ->
          if CicReduction.are_convertible s hety then
           (CicReduction.fdebug := -1 ;
-          eat_prods (CicSubstitution.subst hete t) tl
+           eat_prods (CicSubstitution.subst hete t) tl
           )
          else
-          (
-          CicReduction.fdebug := 0 ;
-          let _ = CicReduction.are_convertible s hety in
-          debug hete [hety ; s] ;
-          raise (NotWellTyped "Appl: wrong parameter-type")
-)
+          begin
+           CicReduction.fdebug := 0 ;
+           ignore (CicReduction.are_convertible s hety) ;
+           fdebug := 0 ;
+           debug s [hety] ;
+           raise (NotWellTyped "Appl: wrong parameter-type")
+          end
       | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
     )
  in