aboutsummaryrefslogtreecommitdiffhomepage
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, 0 insertions, 2 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index f20c0dd83..b417dc1d4 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -907,8 +907,6 @@ let whd_programs_stack env sigma =
let whd_programs env sigma x =
zip (whd_programs_stack env sigma (x, empty_stack))
-exception IsType
-
let find_conclusion env sigma =
let rec decrec env c =
let t = whd_betadeltaiota env sigma c in