 21 Dec, 2018 7 commits


Robbert authored
The unbounded fractional camera See merge request FP/iriscoq!195

Robbert Krebbers authored

Robbert Krebbers authored
 More consistent indentation.  Mark new subgoals as comments.

Robbert Krebbers authored

Robbert Krebbers authored

Robbert authored
Lemmas about subst_map on closed expressions See merge request FP/iriscoq!194

Dan Frumin authored

 20 Dec, 2018 5 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 19 Dec, 2018 1 commit


Ralf Jung authored

 18 Dec, 2018 2 commits


Robbert authored
Two small lemmas about binder_insert See merge request FP/iriscoq!193

Dan Frumin authored

 15 Dec, 2018 1 commit


Ralf Jung authored

 14 Dec, 2018 1 commit


Robbert Krebbers authored

 13 Dec, 2018 4 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
This is to avoid confusion with those of selection patterns.

 12 Dec, 2018 4 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 10 Dec, 2018 7 commits


Robbert Krebbers authored
This lemma is similar to `later_ownM`.

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
This lemma allows one to get the witness out of a later, without having to use `later_car`, i.e. in a way that works in the onpaper version of the logic.

Robbert Krebbers authored

 08 Dec, 2018 1 commit


Robbert Krebbers authored

 07 Dec, 2018 3 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 06 Dec, 2018 1 commit


Robbert Krebbers authored
Thanks to @Blaisorblade for reporting.

 03 Dec, 2018 2 commits


Robbert Krebbers authored
Thanks @jtassaro.

Robbert Krebbers authored

 30 Nov, 2018 1 commit


Ralf Jung authored
link to coqdoc See merge request FP/iriscoq!192
