aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--proofs/pfedit.ml4
-rw-r--r--test-suite/bugs/closed/7795.v65
-rw-r--r--test-suite/output/UnivBinders.out18
-rw-r--r--test-suite/output/UnivBinders.v5
-rw-r--r--vernac/vernacentries.ml35
5 files changed, 102 insertions, 25 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 678c3ea3f7..d971c28a26 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -173,8 +173,8 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
const_entry_body = Future.chain ce.const_entry_body
(fun (pt, _) -> pt, ()) } in
let (cb, ctx), () = Future.force ce.const_entry_body in
- let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in
- cb, status, Evd.evar_universe_context univs'
+ let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in
+ cb, status, univs
let refine_by_tactic env sigma ty tac =
(** Save the initial side-effects to restore them afterwards. We set the
diff --git a/test-suite/bugs/closed/7795.v b/test-suite/bugs/closed/7795.v
new file mode 100644
index 0000000000..5db0f81cc5
--- /dev/null
+++ b/test-suite/bugs/closed/7795.v
@@ -0,0 +1,65 @@
+
+
+Definition fwd (b: bool) A (e2: A): A. Admitted.
+
+Ltac destruct_refinement_aux T :=
+ let m := fresh "mres" in
+ let r := fresh "r" in
+ let P := fresh "P" in
+ pose T as m;
+ destruct m as [ r P ].
+
+Ltac destruct_refinement :=
+ match goal with
+ | |- context[proj1_sig ?T] => destruct_refinement_aux T
+ end.
+
+Ltac t_base := discriminate || destruct_refinement.
+
+
+Inductive List (T: Type) :=
+| Cons_construct: T -> List T -> List T
+| Nil_construct: List T.
+
+Definition t (T: Type): List T. Admitted.
+Definition size (T: Type) (src: List T): nat. Admitted.
+Definition filter1_rt1_type (T: Type): Type := { res: List T | false = true }.
+Definition filter1 (T: Type): filter1_rt1_type T. Admitted.
+
+Definition hh_1:
+ forall T : Type,
+ (forall (T0 : Type),
+ False -> filter1_rt1_type T0) ->
+ False.
+Admitted.
+
+Definition hh_2:
+ forall (T : Type),
+ filter1_rt1_type T ->
+ filter1_rt1_type T.
+Admitted.
+
+Definition hh:
+ forall (T : Type) (f1 : forall (T0 : Type), False -> filter1_rt1_type T0),
+ fwd
+ (Nat.leb
+ (size T
+ (fwd false (List T)
+ (fwd false (List T)
+ (proj1_sig
+ (hh_2 T
+ (f1 T (hh_1 T f1))))))) 0) bool
+ false = true.
+Admitted.
+
+Set Program Mode. (* removing this line prevents the bug *)
+Obligation Tactic := repeat t_base.
+
+Goal
+ forall T (h17: T),
+ filter1 T =
+ exist
+ _
+ (Nil_construct T)
+ (hh T (fun (T : Type) (_ : False) => filter1 T)).
+Abort.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 6f41b2fcf9..926114a1e1 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -48,6 +48,12 @@ Type@{Top.17} -> Type@{v} -> Type@{u}
(* u Top.17 v |= *)
foo is universe polymorphic
+Type@{i} -> Type@{j}
+ : Type@{max(i+1,j+1)}
+(* {j i} |= *)
+ = Type@{i} -> Type@{j}
+ : Type@{max(i+1,j+1)}
+(* {j i} |= *)
Monomorphic mono = Type@{mono.u}
: Type@{mono.u+1}
(* {mono.u} |= *)
@@ -149,24 +155,24 @@ inmod@{u} -> Type@{v}
(* u v |= *)
Applied.infunct is universe polymorphic
-axfoo@{i Top.44 Top.45} : Type@{Top.44} -> Type@{i}
-(* i Top.44 Top.45 |= *)
+axfoo@{i Top.48 Top.49} : Type@{Top.48} -> Type@{i}
+(* i Top.48 Top.49 |= *)
axfoo is universe polymorphic
Argument scope is [type_scope]
Expands to: Constant Top.axfoo
-axbar@{i Top.44 Top.45} : Type@{Top.45} -> Type@{i}
-(* i Top.44 Top.45 |= *)
+axbar@{i Top.48 Top.49} : Type@{Top.49} -> Type@{i}
+(* i Top.48 Top.49 |= *)
axbar is universe polymorphic
Argument scope is [type_scope]
Expands to: Constant Top.axbar
-axfoo' : Type@{Top.47} -> Type@{axbar'.i}
+axfoo' : Type@{Top.51} -> Type@{axbar'.i}
axfoo' is not universe polymorphic
Argument scope is [type_scope]
Expands to: Constant Top.axfoo'
-axbar' : Type@{Top.47} -> Type@{axbar'.i}
+axbar' : Type@{Top.51} -> Type@{axbar'.i}
axbar' is not universe polymorphic
Argument scope is [type_scope]
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index c6efc240a6..f806a9f4f7 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -30,6 +30,11 @@ Unset Strict Universe Declaration.
order of appearance. *)
Definition foo@{u +} := Type -> Type@{v} -> Type@{u}.
Print foo.
+
+Check Type@{i} -> Type@{j}.
+
+Eval cbv in Type@{i} -> Type@{j}.
+
Set Strict Universe Declaration.
(* Binders even work with monomorphic definitions! *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e1c9712135..f7ba305374 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1692,36 +1692,37 @@ let query_command_selector ?loc = function
let vernac_check_may_eval ~atts redexp glopt rc =
let glopt = query_command_selector ?loc:atts.loc glopt in
let (sigma, env) = get_current_context_of_args glopt in
- let sigma', c = interp_open_constr env sigma rc in
- let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in
- Evarconv.check_problems_are_solved env sigma';
- let sigma' = Evd.minimize_universes sigma' in
- let uctx = Evd.universe_context_set sigma' in
- let env = Environ.push_context_set uctx (Evarutil.nf_env_evar sigma' env) in
+ let sigma, c = interp_open_constr env sigma rc in
+ let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
+ Evarconv.check_problems_are_solved env sigma;
+ let sigma = Evd.minimize_universes sigma in
+ let uctx = Evd.universe_context_set sigma in
+ let env = Environ.push_context_set uctx (Evarutil.nf_env_evar sigma env) in
let j =
- if Evarutil.has_undefined_evars sigma' c then
- Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c)
+ if Evarutil.has_undefined_evars sigma c then
+ Evarutil.j_nf_evar sigma (Retyping.get_judgment_of env sigma c)
else
- let c = EConstr.to_constr sigma' c in
+ let c = EConstr.to_constr sigma c in
(* OK to call kernel which does not support evars *)
Termops.on_judgment EConstr.of_constr (Arguments_renaming.rename_typing env c)
in
- match redexp with
+ let pp = match redexp with
| None ->
- let evars_of_term c = Evarutil.undefined_evars_of_term sigma' c in
+ let evars_of_term c = Evarutil.undefined_evars_of_term sigma c in
let l = Evar.Set.union (evars_of_term j.Environ.uj_val) (evars_of_term j.Environ.uj_type) in
- let j = { j with Environ.uj_type = Reductionops.nf_betaiota env sigma' j.Environ.uj_type } in
- print_judgment env sigma' j ++
- pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++
- Printer.pr_universe_ctx_set sigma uctx
+ let j = { j with Environ.uj_type = Reductionops.nf_betaiota env sigma j.Environ.uj_type } in
+ print_judgment env sigma j ++
+ pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma l
| Some r ->
- let (sigma',r_interp) = Hook.get f_interp_redexp env sigma' r in
+ let (sigma,r_interp) = Hook.get f_interp_redexp env sigma r in
let redfun env evm c =
let (redfun, _) = reduction_of_red_expr env r_interp in
let (_, c) = redfun env evm c in
c
in
- print_eval redfun env sigma' rc j
+ print_eval redfun env sigma rc j
+ in
+ pp ++ Printer.pr_universe_ctx_set sigma uctx
let vernac_declare_reduction ~atts s r =
let local = make_locality atts.locality in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 16:12:23 +0000