aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pattern.ml
diff options
context:
space:
mode:
authorMaxime Dénès2020-04-21 13:21:09 +0200
committerMaxime Dénès2020-04-21 13:21:09 +0200
commitdcced70a3ac146efb2f6214e197ef4b0d73debb1 (patch)
tree6009d4f34f3af2923de51ee853d2085b1d657200 /pretyping/pattern.ml
parent2fdca75132b7d8495b7df5b10bbd9dde05fd5190 (diff)
parente89cf30983d3af97607885413a4a8eaaa071fa52 (diff)
Merge PR #11896: Use lists instead of arrays in evar instances.
Ack-by: SkySkimmer Reviewed-by: maximedenes
Diffstat (limited to 'pretyping/pattern.ml')
-rw-r--r--pretyping/pattern.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 3f2e690da5..1dfb8b2cd1 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -24,7 +24,7 @@ type case_info_pattern =
type constr_pattern =
| PRef of GlobRef.t
| PVar of Id.t
- | PEvar of Evar.t * constr_pattern array
+ | PEvar of constr_pattern Constr.pexistential
| PRel of int
| PApp of constr_pattern * constr_pattern array
| PSoApp of patvar * constr_pattern list