diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-15 13:01:10 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-15 13:01:10 +0000 |
| commit | c6a4c593148f72aa5de5294c82b4dcd42be078c8 (patch) | |
| tree | 3064e13ebb5728abcb6532486700fc2542f87bc7 | |
| parent | 404761b484dabbdc3025e5c2df91b15968b12c62 (diff) | |
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
| -rw-r--r-- | pretyping/cases.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 42569c9ce..39191f395 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 |