X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=fbcf25f91450a4beb8ace412ba213dcfc0fa0d6c;hb=acf29bdbdcdc6ad8c2d9d27e8a47500981b605cd;hp=fe46e474849861fdfac7fa879d90e2322bcf7af3;hpb=0575a1cb077087970f311b48f2e45dc4a01a6867;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index fe46e4748..fbcf25f91 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -42,7 +42,7 @@ let debug t context =
    raise (TypeCheckerFailure (List.fold_right debug_aux (t::context) ""))
 ;;
 
-let debug_print = prerr_endline ;;
+let debug_print = fun _ -> () ;;
 
 let rec split l n =
  match (l,n) with
@@ -184,7 +184,7 @@ let rec type_of_constant ~logger uri ugraph =
                CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
              | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
 	 with Invalid_argument s ->
-	   (*prerr_endline s;*)
+	   (*debug_print s;*)
 	   uobj,ugraph_dust       
   in
    match cobj,ugraph with
@@ -225,7 +225,7 @@ and type_of_variable ~logger uri ugraph =
 	     | CicEnvironment.CheckedObj _ 
              | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
          with Invalid_argument s ->
-           (*prerr_endline s;*)
+           (*debug_print s;*)
            ty,ugraph2)
    |  _ ->
 	raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri))
@@ -574,7 +574,7 @@ and type_of_mutual_inductive_defs ~logger uri i ugraph =
 	     )
 	   with
 	       Invalid_argument s ->
-		 (*prerr_endline s;*)
+		 (*debug_print s;*)
 		 uobj,ugraph1_dust
   in
     match cobj with
@@ -609,7 +609,7 @@ and type_of_mutual_inductive_constr ~logger uri i j ugraph =
 		       raise CicEnvironmentError)
 	    with
 		Invalid_argument s ->
-		  (*prerr_endline s;*)
+		  (*debug_print s;*)
 		  uobj,ugraph1_dust
   in
     match cobj with
@@ -903,7 +903,7 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
        (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
        exp_named_subst true
    | C.MutCase (uri,i,outtype,term,pl) ->
-      (match term with
+      (match CicReduction.whd context term with
           C.Rel m when List.mem m safes || m = x ->
            let (tys,len,isinductive,paramsno,cl) =
 	    let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
@@ -1680,8 +1680,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
               else raise 
 		(TypeCheckerFailure 
 		   (sprintf
-		      ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}")
-		      (CicPp.ppterm typ) (U.string_of_uri uri) i))
+		      ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
+		      (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))
           | C.Appl 
 	      ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
               if U.eq uri uri' && i = i' then
@@ -1691,8 +1691,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
               else raise 
 		(TypeCheckerFailure 
 		   (sprintf
-		      "Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}"
-		      (CicPp.ppterm typ') (U.string_of_uri uri) i))
+		      ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
+		      (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))
           | _ ->
               raise 
 		(TypeCheckerFailure 
@@ -2037,12 +2037,12 @@ let typecheck uri ugraph =
    (* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *)
    match CicEnvironment.is_type_checked ~trust:false ugraph uri with
      CicEnvironment.CheckedObj (cobj,ugraph') -> 
-       (* prerr_endline ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*)
+       (* debug_print ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*)
        cobj,ugraph'
    | CicEnvironment.UncheckedObj uobj ->
       (* let's typecheck the uncooked object *)
       logger#log (`Start_type_checking uri) ;
-      (* prerr_endline ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *)
+      (* debug_print ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *)
       let ugraph1 = 
 	(match uobj with
          C.Constant (_,Some te,ty,_,_) ->
@@ -2111,7 +2111,7 @@ let typecheck uri ugraph =
 	      object.
 	    *)
 	    Invalid_argument s -> 
-	      (*prerr_endline s;*)
+	      (*debug_print s;*)
 	      uobj,ugraph1
 ;;