minor changes to make the library compile after wilmers new exists.

[helm.git] / helm / software / components / ng_kernel / nCicTypeChecker.ml

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index c09b036b67b21a9e93675cd6bb07eab59b02a81f..a4ff68d9fc4ae745488b63c220cd2718a167f1d9 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -126,7 +126,8 @@ let sort_of_prod ~metasenv ~subst context (name,s) t (t1, t2) =
    let t2 = R.whd ~subst ((name,C.Decl s)::context) t2 in
    match t1, t2 with
    | C.Sort _, C.Sort C.Prop -> t2
-   | C.Sort (C.Type u1), C.Sort (C.Type u2) -> C.Sort (C.Type (u1@u2)) 
+   | C.Sort (C.Type u1), C.Sort (C.Type u2) ->
+      C.Sort (C.Type (NCicEnvironment.max u1 u2))
    | C.Sort C.Prop,C.Sort (C.Type _) -> t2
    | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))), C.Sort _ -> t2
    | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))), C.Meta (i,(_,(C.Irl 0 | C.Ctx [])))
@@ -677,7 +678,7 @@ and eat_prods ~subst ~metasenv context he ty_he args_with_ty =
             raise 
               (TypeCheckerFailure 
                 (lazy (Printf.sprintf
-                  ("Appl: wrong application of %s: the parameter %s has type"^^
+                  ("Appl: wrong application of %s: the argument %s has type"^^
                    "\n%s\nbut it should have type \n%s\nContext:\n%s\n")
                   (PP.ppterm ~subst ~metasenv ~context he)
                   (PP.ppterm ~subst ~metasenv ~context arg)
@@ -1302,4 +1303,31 @@ E.set_typecheck_obj
 
 let _ = NCicReduction.set_get_relevance get_relevance;;
 
+
+let indent = ref 0;;
+let debug = true;;
+let logger =
+    let do_indent () = String.make !indent ' ' in  
+    (function 
+      | `Start_type_checking s ->
+          if debug then
+           prerr_endline (do_indent () ^ "Start: " ^ NUri.string_of_uri s); 
+          incr indent
+      | `Type_checking_completed s ->
+          decr indent;
+          if debug then
+           prerr_endline (do_indent () ^ "End: " ^ NUri.string_of_uri s)
+      | `Type_checking_interrupted s ->
+          decr indent;
+          if debug then
+           prerr_endline (do_indent () ^ "Break: " ^ NUri.string_of_uri s)
+      | `Type_checking_failed s ->
+          decr indent;
+          if debug then
+           prerr_endline (do_indent () ^ "Fail: " ^ NUri.string_of_uri s)
+      | `Trust_obj s ->
+          if debug then
+           prerr_endline (do_indent () ^ "Trust: " ^ NUri.string_of_uri s))
+;;
+(* let _ = set_logger logger ;; *)
 (* EOF *)