Just code clean-up.

diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml
index e0ad91f59b2414c3c855fb07287edc0f0e341c88..395d7a69693340fa037124c810e5cd3648b11b2f 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReduction.ml
+++ b/helm/ocaml/cic_proof_checking/cicReduction.ml
@@ -202,7 +202,7 @@ let are_convertible t1 t2 =
      let t1' = whd t1 
      and t2' = whd t2 in
      debug t1' [t2'] "POSTWHD";
-     (*if !fdebug = 0 then ignore(Unix.system "read" );*)
+let res =
       match (t1',t2') with
          (C.Rel n1, C.Rel n2) -> n1 = n2
        | (C.Var uri1, C.Var uri2) -> U.eq uri1 uri2
@@ -262,6 +262,8 @@ let are_convertible t1 t2 =
        | (_,_) ->
           debug t1' [t2'] "NOT-CONVERTIBLE" ;
           false
+in
+if res then true else (debug t1' [t2'] "NOT-CONVERTIBLE" ; false)
    end
  in
   aux t1 t2

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