diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-02 15:03:28 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-02 16:17:30 +0200 |
| commit | 6a736c77dee9315afd6d5f50375bf92c1da5d20c (patch) | |
| tree | 1047b1578024ad227679d025714620bd611120d4 /pretyping | |
| parent | 351adedc4d154f9f60a3a01b2e906ce2063e323f (diff) | |
Completing fixing order of parameters when translating from
glob_constr to constr_pattern. Was partially fixed to solve #3088
(8e88b7adab) in but the order of lambdas was still incorrect as the
fix of the order of lambdas in second-order pattern-matching for #3136
showed (83159124ce22).
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/patternops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 3e43853a5..dc7aa848c 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -378,7 +378,7 @@ let rec pat_of_raw metas vars = function in let pred = match p,indnames with | Some p, Some (_,_,nal) -> - let nvars = List.rev_append nal (na :: vars) in + let nvars = na :: List.rev nal @ vars in rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p)) | _ -> PMeta None in |