 14 Jun, 2016 4 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 08 Jun, 2016 1 commit


Robbert Krebbers authored

 07 Jun, 2016 2 commits
 06 Jun, 2016 1 commit


Robbert Krebbers authored

 01 Jun, 2016 17 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

JacquesHenri Jourdan authored

JacquesHenri Jourdan authored

JacquesHenri Jourdan authored

Robbert Krebbers authored

JacquesHenri Jourdan authored

JacquesHenri Jourdan authored

Robbert Krebbers authored
We used => before, which is strange, because it has another meaning in ssreflect.

Robbert Krebbers authored
And use slice_name, which is defined as gname but Opaque, instead of gname in boxes.

Robbert Krebbers authored
They mess up the proof mode notations due to overlaps.

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
Generating a fresh name consists of two stages: + Use [cbv] to compute a list representing the domain of the environment. This is a very simply computation that just erases the hypotheses. + Use [vm_compute] to compute a fresh name based on the list representing the domain. The domain itself should never contain evars, so [vm_compute] will do the job.

Robbert Krebbers authored

Robbert Krebbers authored

 31 May, 2016 15 commits


JacquesHenri Jourdan authored

JacquesHenri Jourdan authored

JacquesHenri Jourdan authored

Robbert Krebbers authored
be the same as
↔ . This is a fairly intrusive change, but at least makes notations more consistent, and often shorter because fewer parentheses are needed. Note that viewshifts already had the same precedence as →. 
Ralf Jung authored

Ralf Jung authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
Now, for example, when having equiv (Some x) (Some y) it will try to find a Proper whose range is an equiv before hitting the eq instance. My hack is general enough that it works for Forall2, dist, and so on, too.

Robbert Krebbers authored
It used to be: (P ={E}=> Q) := (True ⊢ (P → ={E}=> Q)) Now it is: (P ={E}=> Q) := (P ⊢ ={E}=> Q)

Robbert Krebbers authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored
