diff options
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 6296347fd0..3bb9b0f6a1 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -229,7 +229,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = in hook, recname, typ in (* XXX: Capturing sigma here... bad bad *) - let hook = Lemmas.mk_hook (hook sigma) in + let hook = DeclareDef.Hook.make (hook sigma) in Obligations.check_evars env sigma; let evars, _, evars_def, evars_typ = Obligations.eterm_obligations env recname sigma 0 def typ |