diff options
| author | Matthieu Sozeau | 2014-04-07 17:29:26 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:59 +0200 |
| commit | 2d6de8b102ea3cd05c5d193190faf787ccb84baa (patch) | |
| tree | 876350b54e58c77b0bb265afa65a04acd0536872 /toplevel/command.ml | |
| parent | d081f9390206c510d9837e2ecd3fa0a0d4ef0b8c (diff) | |
Fix restrict_universe_context removing some universes that do appear in the term.
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index a11e3a2cd3..2d82b93523 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -257,7 +257,7 @@ let do_assumptions kind nl l = let t = replace_vars subst t in let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) imps false nl in let subst' = List.map2 - (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u))) (*FIXME incorrect should also enrich the context of the current assumption with c's context *) + (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u))) idl refs in (subst'@subst, status' && status)) ([],true) l) |