diff options
| -rw-r--r-- | contrib/subtac/subtac_obligations.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index 941a7576e8..769aff9dcf 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -135,7 +135,7 @@ let declare_definition prg = with _ -> ()); let ce = { const_entry_body = body; - const_entry_type = Some prg.prg_type; + const_entry_type = Some (Termops.refresh_universes prg.prg_type); const_entry_opaque = false; const_entry_boxed = false} in |