diff options
| author | Hugo Herbelin | 2015-05-13 09:11:22 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-05-13 09:56:04 +0200 |
| commit | 574b4096517b4ac9189c2226e1cd75745e788db0 (patch) | |
| tree | 704c3c3f4f21fe2ca94e0929eb93c7d99e317512 /pretyping | |
| parent | d17090cee488844fddc444fdba4fd195c27707c7 (diff) | |
Better fixing #4198 such that the term to match is looked for before
the predicate, thus respecting the visual left-to-right top-down order
(see a45bd5981092).
This fixes CFGV.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/constr_matching.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 5098665582..a0493777a5 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -419,7 +419,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = | [] -> assert false | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) in - let sub = (env, hd) :: (env, c1) :: subargs env lc in + let sub = (env, c1) :: (env, hd) :: subargs env lc in try_aux sub next_mk_ctx next | Fix (indx,(names,types,bodies)) -> let nb_fix = Array.length types in |