Skip to content
Snippets Groups Projects
Commit 616b4062 authored by Ralf Jung's avatar Ralf Jung
Browse files

ref tests: normalize subgoal to goal

parent c5676b11
No related branches found
No related tags found
No related merge requests found
# adjust for https://github.com/coq/coq/pull/13656
s/subgoal/goal/g
1 subgoal
1 goal
X : tele
α, β, γ1, γ2 : X → Prop
============================
accessor α β γ1 → accessor α β (λ.. x : X, γ1 x ∨ γ2 x)
1 subgoal
1 goal
X : tele
α, β, γ1, γ2 : X → Prop
============================
∀.. x : X, γ1 x → (λ.. x0 : X, γ1 x0 ∨ γ2 x0) x
1 subgoal
1 goal
X : tele
α, β, γ1, γ2 : X → Prop
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment