Seed reset before each convert_obj.

[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 907dd8b6cf3c8e8254f5adb165980d86b37904d6..125b66ed35cbd73a945a20a99f4d9d90df1dd8ac 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -539,11 +539,11 @@ let sort_of_prod ~metasenv ~subst context (name,s) (t1, t2) =
          (NCicPp.ppterm ~subst ~metasenv ~context t2))))
 ;;
 
-let eat_prods ~subst ~metasenv context ty_he args_with_ty = 
+let eat_prods ~subst ~metasenv context he ty_he args_with_ty = 
   let rec aux ty_he = function 
   | [] -> ty_he
   | (arg, ty_arg)::tl ->
-      (match R.whd ~subst context ty_he with 
+      match R.whd ~subst context ty_he with 
       | C.Prod (n,s,t) ->
 (*
           prerr_endline (NCicPp.ppterm ~subst ~metasenv ~context s ^ " - Vs - "
@@ -557,13 +557,20 @@ let eat_prods ~subst ~metasenv context ty_he args_with_ty =
             raise 
               (TypeCheckerFailure 
                 (lazy (Printf.sprintf
-                  ("Appl: wrong parameter-type, expected %s, found %s")
-                  (NCicPp.ppterm ~subst ~metasenv ~context ty_arg) 
-                  (NCicPp.ppterm ~subst ~metasenv ~context s))))
+                  ("Appl: wrong parameter-type, expected\n%s\nfound\n%s")
+                  (NCicPp.ppterm ~subst ~metasenv ~context s)
+                  (NCicPp.ppterm ~subst ~metasenv ~context ty_arg))))
        | _ ->
           raise 
             (TypeCheckerFailure
-              (lazy "Appl: this is not a function, it cannot be applied")))
+              (lazy (Printf.sprintf
+                "Appl: %s is not a function, it cannot be applied"
+                (NCicPp.ppterm ~subst ~metasenv ~context
+                 (let res = List.length tl in
+                  let eaten = List.length args_with_ty - res in
+                   (NCic.Appl
+                    (he::List.map fst
+                     (fst (HExtlib.split_nth eaten args_with_ty)))))))))
   in
     aux ty_he args_with_ty
 ;;
@@ -677,7 +684,7 @@ let rec typeof ~subst ~metasenv context term =
        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
+       eat_prods ~subst ~metasenv context he ty_he args_with_ty
    | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
    | C.Match (Ref.Ref (_,_,Ref.Ind tyno) as r,outtype,term,pl) ->
       let outsort = typeof_aux context outtype in
@@ -750,8 +757,8 @@ let rec typeof ~subst ~metasenv context term =
           (lazy (Printf.sprintf ("Branch for constructor %s :=\n%s\n"^^
           "has type %s\nnot convertible with %s") 
           (NCicPp.ppterm  ~subst ~metasenv ~context
-            (C.Const (Ref.mk_constructor j r)))
-          (NCicPp.ppterm ~metasenv ~subst ~context (List.nth pl (j-1)))
+            (C.Const (Ref.mk_constructor (j-1) r)))
+          (NCicPp.ppterm ~metasenv ~subst ~context (List.nth pl (j-2)))
           (NCicPp.ppterm ~metasenv ~subst ~context p_ty) 
           (NCicPp.ppterm ~metasenv ~subst ~context exp_p_ty)))); 
       let res = outtype::arguments@[term] in