diff options
| author | msozeau | 2007-11-04 13:10:56 +0000 |
|---|---|---|
| committer | msozeau | 2007-11-04 13:10:56 +0000 |
| commit | 24f8331a3bc9631c37f162826514e6cb7d679a16 (patch) | |
| tree | 8532b8fc817cb209df2c94e9d7a4429ba5168e93 | |
| parent | e38fc39f64d8af81fc237889329953bfafa29422 (diff) | |
Fix bug#1739
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10286 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |