diff options
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 76ea462c7..57f2571c5 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -42,7 +42,7 @@ let do_universe l = Declare.do_universe l let do_constraint l = Declare.do_constraint l let rec under_binders env f n c = - if Int.equal n 0 then f env Evd.empty c else + if Int.equal n 0 then snd (f env Evd.empty c) else match kind_of_term c with | Lambda (x,t,c) -> mkLambda (x,t,under_binders (push_rel (x,None,t) env) f (n-1) c) |