aboutsummaryrefslogtreecommitdiff
path: root/pretyping/reductionops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/reductionops.ml')
-rw-r--r--pretyping/reductionops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 834c27969e..e8acd67caf 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -770,7 +770,7 @@ let splay_arity env sigma c =
| Sort s -> l,s
| _ -> invalid_arg "splay_arity"
-let sort_of_arity env c = snd (splay_arity env Evd.empty c)
+let sort_of_arity env sigma c = snd (splay_arity env sigma c)
let splay_prod_n env sigma n =
let rec decrec env m ln c = if m = 0 then (ln,c) else