diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-07-17 07:47:31 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-07-17 07:47:31 +0200 |
| commit | 3a5dd0df47b83a1a46061f2a14761d3d9ad79fcb (patch) | |
| tree | 843408d6fa6a37307c0441d7fa81b3df6ae277e2 /plugins/funind/recdef.ml | |
| parent | 0c297ad43bd4b0b8187aa56756334bd294a212ca (diff) | |
| parent | b21cd4620e0983a23dd11c0f582bf367662aeee3 (diff) | |
Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layers
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 1705cac78..bc550c8b9 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -90,7 +90,7 @@ let type_of_const sigma t = |_ -> assert false let constr_of_global x = - fst (Universes.unsafe_constr_of_global x) + fst (Global.constr_of_global_in_context (Global.env ()) x) let constant sl s = constr_of_global (find_reference sl s) |