diff options
| -rw-r--r-- | pretyping/evarsolve.ml | 4 | ||||
| -rw-r--r-- | pretyping/evarsolve.mli | 3 | ||||
| -rw-r--r-- | pretyping/typing.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3330.v (renamed from test-suite/bugs/opened/3330.v) | 66 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3331.v (renamed from test-suite/bugs/opened/3331.v) | 15 |
5 files changed, 54 insertions, 36 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 26e96af48..9522f9c24 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -42,7 +42,7 @@ let get_polymorphic_positions f = templ.template_param_levels) | _ -> assert false -let refresh_universes dir env evd t = +let refresh_universes ?(onlyalg=false) dir env evd t = let evdref = ref evd in let modified = ref false in let rec refresh dir t = @@ -50,7 +50,7 @@ let refresh_universes dir env evd t = | Sort (Type u as s) when (match Univ.universe_level u with | None -> true - | Some l -> Option.is_empty (Evd.is_sort_variable evd s)) -> + | Some l -> not onlyalg && Option.is_empty (Evd.is_sort_variable evd s)) -> (* s' will appear in the term, it can't be algebraic *) let s' = evd_comb0 (new_sort_variable Evd.univ_flexible) evdref in let evd = diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 988938272..6de8f5c8d 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -34,7 +34,8 @@ type conv_fun_bool = val evar_define : conv_fun -> ?choose:bool -> ?dir:bool -> env -> evar_map -> bool option -> existential -> constr -> evar_map -val refresh_universes : bool (* direction: true for levels lower than the existing levels *) -> +val refresh_universes : ?onlyalg:bool (* Only algebraic universes *) -> + bool (* direction: true for levels lower than the existing levels *) -> env -> evar_map -> types -> evar_map * types val solve_refl : ?can_drop:bool -> conv_fun_bool -> env -> evar_map -> diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 7702355b8..1c41a5bb3 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -290,7 +290,7 @@ let e_type_of ?(refresh=false) env evd c = let j = execute env evdref c in (* side-effect on evdref *) if refresh then - Evarsolve.refresh_universes false env !evdref j.uj_type + Evarsolve.refresh_universes ~onlyalg:true false env !evdref j.uj_type else !evdref, j.uj_type let solve_evars env evdref c = diff --git a/test-suite/bugs/opened/3330.v b/test-suite/bugs/closed/3330.v index face3b2d5..0bd3033ac 100644 --- a/test-suite/bugs/opened/3330.v +++ b/test-suite/bugs/closed/3330.v @@ -1,4 +1,29 @@ (* File reduced by coq-bug-finder from original input, then from 12106 lines to 1070 lines *) +Set Universe Polymorphism. +Definition setleq (A : Type@{i}) (B : Type@{j}) := A : Type@{j}. + +Inductive foo : Type@{l} := bar : foo . +Section MakeEq. + Variables (a : foo@{i}) (b : foo@{j}). + + Let t := $(let ty := type of b in exact ty)$. + Definition make_eq (x:=b) := a : t. +End MakeEq. + +Definition same (x : foo@{i}) (y : foo@{i}) := x. + +Section foo. + + Variables x : foo@{i}. + Variables y : foo@{j}. + + Let AleqB := let foo := make_eq x y in (Type * Type)%type. + + Definition baz := same x y. +End foo. + +Definition baz' := Eval unfold baz in baz@{i j k l}. + Module Export HoTT_DOT_Overture. Module Export HoTT. Module Export Overture. @@ -1041,33 +1066,30 @@ Section Adjunction. Variable D : PreCategory. Variable F : Functor C D. Variable G : Functor D C. - Let Adjunction_Type := Eval simpl in hom_functor D o (F^op, 1) <~=~> hom_functor C o (1, G). -End Adjunction. -Undo. + Let Adjunction_Type := + Eval simpl in (hom_functor D) o (F^op, 1) <~=~> (hom_functor C) o (1, G). Record AdjunctionHom := { - mate_of : @NaturalIsomorphism - H - (Category.Prod.prod (Category.Dual.opposite C) D) - (@Core.set_cat H) - (@compose - (Category.Prod.prod (Category.Dual.opposite C) D) - (Category.Prod.prod (Category.Dual.opposite D) D) - (@Core.set_cat H) (@hom_functor H D) - (@pair (Category.Dual.opposite C) - (Category.Dual.opposite D) D D - (@opposite C D F) (identity D))) - (@compose - (Category.Prod.prod (Category.Dual.opposite C) D) - (Category.Prod.prod (Category.Dual.opposite C) C) - (@Core.set_cat H) (@hom_functor H C) - (@pair (Category.Dual.opposite C) - (Category.Dual.opposite C) D C - (identity (Category.Dual.opposite C)) G)) + mate_of : + @NaturalIsomorphism H + (Prod.prod (Category.Dual.opposite C) D) + (@set_cat H) + (@compose (Prod.prod (Category.Dual.opposite C) D) + (Prod.prod (Category.Dual.opposite D) D) + (@set_cat H) (@hom_functor H D) + (@pair (Category.Dual.opposite C) + (Category.Dual.opposite D) D D + (@opposite C D F) (identity D))) + (@compose (Prod.prod (Category.Dual.opposite C) D) + (Prod.prod (Category.Dual.opposite C) C) + (@set_cat H) (@hom_functor H C) + (@pair (Category.Dual.opposite C) + (Category.Dual.opposite C) D C + (identity (Category.Dual.opposite C)) G)) }. -Fail End Adjunction. +End Adjunction. (* Error: Illegal application: The term "NaturalIsomorphism" of type "forall (H : Funext) (C D : PreCategory), diff --git a/test-suite/bugs/opened/3331.v b/test-suite/bugs/closed/3331.v index 07504aed7..9cd44bd0c 100644 --- a/test-suite/bugs/opened/3331.v +++ b/test-suite/bugs/closed/3331.v @@ -24,13 +24,8 @@ Section groupoid_category. compute in H. change (forall (x y : X) (p q : x = y) (r s : p = q), Contr (r = s)) in H. assert (H' := H). - pose proof (_ : Contr (idpath = idpath :> (@paths (@paths X d d) idpath idpath))) as X0. (* success *) - clear H' X0. - Fail pose (_ : Contr (idpath = idpath :> (@paths (@paths X d d) idpath idpath))). (* Toplevel input, characters 21-22: -Error: -Cannot infer this placeholder. -Could not find an instance for "Contr (idpath = idpath)" in environment: - -X : Type -H : forall (x y : X) (p q : x = y) (r s : p = q), Contr (r = s) -d : X *) + set (foo:=_ : Contr (idpath = idpath :> (@paths (@paths X d d) idpath idpath))). (* success *) + clear H' foo. + Set Typeclasses Debug. + pose (_ : Contr (idpath = idpath :> (@paths (@paths X d d) idpath idpath))). +Abort.
\ No newline at end of file |