diff options
| author | Emilio Jesus Gallego Arias | 2019-02-24 20:38:21 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-17 12:30:13 +0200 |
| commit | 873281c256fc33941d93044acc3db8eda0a148ee (patch) | |
| tree | 2104c16c197b2cc9a8c9cc903818691b6eb1a3a7 /vernac/comProgramFixpoint.ml | |
| parent | 7dc04f0244aeb277b62070f87590cbc2cafd8396 (diff) | |
[proof] Move declaration hooks to DeclareDef.
This way both `Lemmas` and `DeclareObl` can depend on it, removing one
more difficulty on the unification of terminators.
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 |