diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/lemmas.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 65655ed90..bf8cbcc25 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -16,6 +16,7 @@ open Pp open Names open Term open Declarations +open Declareops open Entries open Environ open Nameops @@ -40,7 +41,7 @@ let retrieve_first_recthm = function (pi2 (Global.lookup_named id),variable_opacity id) | ConstRef cst -> let cb = Global.lookup_constant cst in - (Option.map Declarations.force (body_of_constant cb), is_opaque cb) + (Option.map Lazyconstr.force (body_of_constant cb), is_opaque cb) | _ -> assert false let adjust_guardness_conditions const = function |