aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/pattern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'intf/pattern.ml')
-rw-r--r--intf/pattern.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/pattern.ml b/intf/pattern.ml
index 20636accf..64873a039 100644
--- a/intf/pattern.ml
+++ b/intf/pattern.ml
@@ -26,7 +26,7 @@ type constr_pattern =
| PRel of int
| PApp of constr_pattern * constr_pattern array
| PSoApp of patvar * constr_pattern list
- | PProj of projection * constr_pattern
+ | PProj of Projection.t * constr_pattern
| PLambda of Name.t * constr_pattern * constr_pattern
| PProd of Name.t * constr_pattern * constr_pattern
| PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern