aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/impargs.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/impargs.ml b/interp/impargs.ml
index a1b029c381..c6405b40fc 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -229,7 +229,7 @@ let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc
let rec is_rigid_head sigma t = match kind sigma t with
| Rel _ | Evar _ -> false
| Ind _ | Const _ | Var _ | Sort _ -> true
- | Case (_,_,f,_) -> is_rigid_head sigma f
+ | Case (_,_,_,f,_) -> is_rigid_head sigma f
| Proj (p,c) -> true
| App (f,args) ->
(match kind sigma f with