From c6a4c593148f72aa5de5294c82b4dcd42be078c8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 15 Oct 2001 13:01:10 +0000
Subject: Insertion automatique des motifs de let-in s'il ne sont pas
 explicitement mentionnés (pour compatibilité) (2 ème)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2118 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/cases.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 42569c9ce3..39191f3953 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -498,7 +498,7 @@ let check_and_adjust_constructor loc (_,j as cstr_sp) mind cstrs pats =
   let nb_args_constr = cstrs.(j-1).cs_nargs in
   if List.length pats = nb_args_constr then pats
   else
-    try adjust_local_defs (pats, cstrs.(j-1).cs_args)
+    try adjust_local_defs (pats, List.rev cstrs.(j-1).cs_args)
     with NotAdjustable ->
       error_wrong_numarg_constructor_loc loc cstr_sp nb_args_constr
 
-- 
cgit v1.2.3