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 | |
| parent | d081f9390206c510d9837e2ecd3fa0a0d4ef0b8c (diff) | |
Fix restrict_universe_context removing some universes that do appear in the term.
| -rw-r--r-- | library/universes.ml | 2 | ||||
| -rw-r--r-- | test-suite/success/polymorphism.v | 4 | ||||
| -rw-r--r-- | toplevel/command.ml | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/library/universes.ml b/library/universes.ml index 2ed477d67b..7d1908d1f5 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -673,7 +673,7 @@ let restrict_universe_context (univs,csts) s = if LSet.mem l diff && LSet.mem r diff then (univs, csts) else (LSet.add l (LSet.add r univs), Constraint.add c csts)) csts (LSet.empty, Constraint.empty) - in (LSet.inter univs univscstrs, csts) + in (LSet.union s (LSet.inter univs univscstrs), csts) let simplify_universe_context (univs,csts) = let uf = UF.create () in diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 7c1166c4c4..1ef2713e44 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -243,7 +243,7 @@ Polymorphic Definition fun_ext (A B : Type) := Polymorphic Class Funext A B := extensional : fun_ext A B. -Section foo. +Section foo2. Context `{forall A B, Funext A B}. Print Universes. -End foo. +End foo2. 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) |