context of types built in the reverse order

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index db79888d5d2265217d9caeb15e43b15f8c7b25ea..9de1f0f5c27203258e4512d6bab0a5e9b8f7598d 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -558,7 +558,7 @@ let eat_prods ~subst ~metasenv context he ty_he args_with_ty =
               (TypeCheckerFailure 
                 (lazy (Printf.sprintf
                   ("Appl: wrong application of %s: the parameter %s has type"^^
-                   "\n%s\nbut is should have type \n%s\n")
+                   "\n%s\nbut it should have type \n%s\n")
                   (NCicPp.ppterm ~subst ~metasenv ~context he)
                   (NCicPp.ppterm ~subst ~metasenv ~context arg)
                   (NCicPp.ppterm ~subst ~metasenv ~context ty_arg)
@@ -951,7 +951,7 @@ and check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl =
   List.iter (fun (_,_,x,_) -> ignore (typeof ~subst ~metasenv [] x)) tyl;
   (* let's check if the types of the inductive constructors are well formed. *)
   let len = List.length tyl in
-  let tys = List.map (fun (_,n,ty,_) -> (n,(C.Decl ty))) tyl in
+  let tys = List.rev (List.map (fun (_,n,ty,_) -> (n,(C.Decl ty))) tyl) in
   ignore
    (List.fold_right
     (fun (_,_,_,cl) i ->