From: Enrico Tassi Date: Fri, 11 Apr 2008 10:16:56 +0000 (+0000) Subject: context of types built in the reverse order X-Git-Tag: make_still_working~5366 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ccb09743430d585f773eb83ad9a18d1dbdda07ed;p=helm.git 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 db79888d5..9de1f0f5c 100644 --- 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 ->