diff options
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) |