Files

 master

/

tests

/

Copy path

Directory actions

More options

Directory actions

More options

Latest commit

jhjourdan

Add comment; fix test tests/heap_lang.v.

Oct 31, 2018

3e0931e · Oct 31, 2018

History

History

/

tests

/

Top

Folders and files

Name		Name	Last commit message	Last commit date
parent directory ..
algebra.ref		algebra.ref	move test suite out of theories/ so it does not get installed; also c…	May 17, 2018
algebra.v		algebra.v	Use unicide ∧ and ∃.	Oct 22, 2018
atomic.ref		atomic.ref	Use telescopes for atomic accessors, updates and triples; improve mas…	Jul 13, 2018
atomic.v		atomic.v	Use telescopes for atomic accessors, updates and triples; improve mas…	Jul 13, 2018
heap_lang.ref		heap_lang.ref	Add comment; fix test tests/heap_lang.v.	Oct 31, 2018
heap_lang.v		heap_lang.v	Add comment; fix test tests/heap_lang.v.	Oct 31, 2018
heap_lang2.ref		heap_lang2.ref	fix yet another case of broken heap_lang notation	Jun 14, 2018
heap_lang2.v		heap_lang2.v	fix yet another case of broken heap_lang notation	Jun 14, 2018
ipm_paper.ref		ipm_paper.ref	make sbi_laterN compute and rely on that instead of MakeLaterN	Jul 3, 2018
ipm_paper.v		ipm_paper.v	wp_pures.	Oct 29, 2018
list_reverse.ref		list_reverse.ref	A specific constructor for injecting values in expressions	Oct 29, 2018
list_reverse.v		list_reverse.v	wp_pures.	Oct 29, 2018
mosel_paper.ref		mosel_paper.ref	tests/mosel_paper: show the two goals separately	Jun 1, 2018
mosel_paper.v		mosel_paper.v	tests/mosel_paper: show the two goals separately	Jun 1, 2018
one_shot.ref		one_shot.ref	A specific constructor for injecting values in expressions	Oct 29, 2018
one_shot.v		one_shot.v	wp_pures.	Oct 29, 2018
proofmode.ref		proofmode.ref	Coq master got 'better' at ltac backtraces, so we have to name some m…	Oct 4, 2018
proofmode.v		proofmode.v	Remove spurious import.	Oct 22, 2018
proofmode_iris.ref		proofmode_iris.ref	Coq master got 'better' at ltac backtraces, so we have to name some m…	Oct 4, 2018
proofmode_iris.v		proofmode_iris.v	Coq master got 'better' at ltac backtraces, so we have to name some m…	Oct 4, 2018
proofmode_monpred.ref		proofmode_monpred.ref	also test the output of error messages	Jun 14, 2018
proofmode_monpred.v		proofmode_monpred.v	monpred test: use typed turnstile notation	Jun 14, 2018
telescopes.ref		telescopes.ref	test and fix more telescope normalization	Jul 3, 2018
telescopes.v		telescopes.v	test and fix more telescope normalization	Jul 3, 2018
tree_sum.ref		tree_sum.ref	move test suite out of theories/ so it does not get installed; also c…	May 17, 2018
tree_sum.v		tree_sum.v	wp_pures.	Oct 29, 2018
View all files