diff options
| author | Maxime Dénès | 2020-04-21 13:21:09 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-04-21 13:21:09 +0200 |
| commit | dcced70a3ac146efb2f6214e197ef4b0d73debb1 (patch) | |
| tree | 6009d4f34f3af2923de51ee853d2085b1d657200 /engine/termops.ml | |
| parent | 2fdca75132b7d8495b7df5b10bbd9dde05fd5190 (diff) | |
| parent | e89cf30983d3af97607885413a4a8eaaa071fa52 (diff) | |
Merge PR #11896: Use lists instead of arrays in evar instances.
Ack-by: SkySkimmer
Reviewed-by: maximedenes
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 16f2a87c1e..6d779e6a35 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -636,8 +636,8 @@ let map_constr_with_binders_left_to_right sigma g f l c = if b' == b then c else mkProj (p, b') | Evar (e,al) -> - let al' = Array.map_left (f l) al in - if Array.for_all2 (==) al' al then c + let al' = List.map_left (f l) al in + if List.for_all2 (==) al' al then c else mkEvar (e, al') | Case (ci,p,b,bl) -> (* In v8 concrete syntax, predicate is after the term to match! *) @@ -707,8 +707,8 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr = let c' = f l c in if c' == c then cstr else mkProj (p, c') | Evar (e,al) -> - let al' = Array.map (f l) al in - if Array.for_all2 (==) al al' then cstr else mkEvar (e, al') + let al' = List.map (f l) al in + if List.for_all2 (==) al al' then cstr else mkEvar (e, al') | Case (ci,p,c,bl) when userview -> let p' = map_return_predicate_with_full_binders sigma g f l ci p in let c' = f l c in |