some debug printings

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 7af5d17a6f6e1e7a950184575784601ca0a700c6..b21274fea109915daca66ea3d1aab10f3501b9d2 100644 (file)
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -42,7 +42,8 @@ let ppobj = function
         (List.map (fun (_,name,n,ty,bo) ->
           name ^ " on " ^ string_of_int n ^ " : " ^ ppterm ty ^ " :=\n"^
           ppterm bo) fl)
-  | _ -> "todo"
+  | (u,_,_,_,NCic.Inductive (b, _,tl, _)) -> "inductive"
+  | (u,_,_,_,NCic.Constant (_,_,_, _, _)) -> "constant"
 ;;
 
 

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 81f633bb6c850362623c0b617ff3ccc41e86b52f..ceb14d17c4145cd432ee4fc3290bb06c8fb1b082 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -608,6 +608,11 @@ let eat_prods ~subst ~metasenv context ty_he args_with_ty =
   | (arg, ty_arg)::tl ->
       (match R.whd ~subst context ty_he with 
       | C.Prod (n,s,t) ->
+(*
+          prerr_endline (NCicPp.ppterm ~context s ^ " - Vs - " ^ NCicPp.ppterm
+          ~context ty_arg);
+          prerr_endline (NCicPp.ppterm ~context (S.subst ~avoid_beta_redexes:true arg t));
+*)
           if R.are_convertible ~subst ~metasenv context ty_arg s then
             aux (S.subst ~avoid_beta_redexes:true arg t) tl
           else
@@ -667,7 +672,9 @@ let does_not_occur ~subst context n nn t =
 exception NotGuarded;;
 
 let rec typeof ~subst ~metasenv context term =
-  let rec typeof_aux context = function
+  let rec typeof_aux context = 
+    fun t -> (*prerr_endline (NCicPp.ppterm ~context t); *)
+    match t with
     | C.Rel n ->
        (try
          match List.nth context (n - 1) with
@@ -720,6 +727,13 @@ let rec typeof ~subst ~metasenv context term =
     | C.Appl (he::(_::_ as args)) ->
        let ty_he = typeof_aux context he in
        let args_with_ty = List.map (fun t -> t, typeof_aux context t) args in
+(*
+       prerr_endline ("HEAD: " ^ NCicPp.ppterm ~context ty_he);
+       prerr_endline ("TARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm
+       ~context) (List.map snd args_with_ty)));
+       prerr_endline ("ARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm
+       ~context) (List.map fst args_with_ty)));
+*)
        eat_prods ~subst ~metasenv context ty_he args_with_ty
    | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
    | C.Match (Ref.Ref (dummy_depth,uri,Ref.Ind tyno) as r,outtype,term,pl) ->
@@ -1167,8 +1181,11 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) =
  assert (metasenv = [] && subst = []);
  match kind with
    | C.Constant (_,_,Some te,ty,_) ->
+      prerr_endline ("TY: " ^ NCicPp.ppterm ty);
+      prerr_endline ("BO: " ^ NCicPp.ppterm te);
       let _ = typeof ~subst ~metasenv [] ty in
       let ty_te = typeof ~subst ~metasenv [] te in
+      prerr_endline "XXXX";
       if not (R.are_convertible ~subst ~metasenv [] ty_te ty) then
        raise (TypeCheckerFailure (lazy (Printf.sprintf
         "the type of the body is not the one expected:\n%s\nvs\n%s"