ada/sparkformal
0
0
Fork 0
mirror of https://github.com/AdaCore/sparkformal.git synced 2026-02-12 12:59:48 -08:00
Code Issues Packages Projects Releases Wiki Activity
161 Commits 3 Branches 1 Tag
master
Commit Graph

161 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
yannickmoy
51ed67be1b Merge pull request #5 from yannickmoy/master 
Add GPLv3 license
 2020-11-12 11:31:58 +01:00
Yannick Moy
cb5f97a772 Add GPLv3 license 2020-11-12 11:30:57 +01:00
yannickmoy
aa7bf8796f Merge pull request #4 from Matafou/coq-8.12 
Porting to coq v8.12.
 2020-11-12 11:24:31 +01:00
Pierre Courtieu
8e025e1a27 Porting to coq v8.12. 2020-10-27 14:15:15 +01:00
Pierre Courtieu
857df65a5e Merge pull request #1 from robblanco/cut_until 
Fix predicate name: cutUntil -> cut_until
 2019-01-10 10:18:11 +01:00
Pierre Courtieu
4f717b84da Merge pull request #3 from robblanco/coq-8.8 
Build with Coq 8.8 (fixing issue #2)
 2019-01-10 10:17:05 +01:00
Rob Blanco
a0676be184 Self-correcting workaround for bug in Coq 8.8 
The original Function definition is protected by a Fail directive, and
the corrected copy without let bindings follows. When the bug is
corrected and Function accepts the original definition, Fail will itself
fail, which will force the restitution of the original definition.
Meanwhile, the workaround can be used.
 2018-08-10 17:14:17 -05:00
Rob Blanco
2c10ed5f76 Fix predicate name: cutUntil -> cut_until 2018-08-08 09:48:19 -05:00
Rob Blanco
b565458660 Fix to build with Coq 8.8 2018-08-08 09:29:23 -05:00
Pierre Courtieu
d1623ff989 adding autonamings. 2018-05-18 15:07:56 +02:00
Pierre Courtieu
4b0bd765d5 Adding lemmas. 2018-05-18 14:20:31 +02:00
Pierre Courtieu
e27de324c4 Adding a few lemmas about stores. 2018-03-26 21:47:59 +02:00
Pierre Courtieu
8a59ef2f8e Fix a typo in the semantics. 2018-01-19 23:24:07 +01:00
Pierre Courtieu
a59a72d34d Finishing porting to coq v8.7. 2017-11-30 17:50:45 +01:00
Yannick Moy
e367a3f5c6 typo 2017-11-22 10:11:18 +01:00
Yannick Moy
b7a9f914d4 Add README 2017-11-22 09:42:11 +01:00
Pierre Courtieu
b6825fc891 New result about NoDup and eqlistA. 2017-07-12 18:12:17 +02:00
Pierre Courtieu
20adfd4cc3 More lemmas on environments. 2017-07-11 22:23:13 +02:00
Pierre Courtieu
2455a7f78e TBC changing the def of NoDup. 2017-07-11 00:18:55 +02:00
Pierre Courtieu
6292180798 One more aux lemma about envs. 2017-07-06 21:47:20 +02:00
Pierre Courtieu
5cb8c48e0f Adding future lemmas, commented. 2017-07-05 22:30:16 +02:00
Pierre Courtieu
be0a26ef1b new lemmas about envs. 2017-07-03 13:56:00 +02:00
Pierre Courtieu
ce944f1d1a Few lemmas on environment. 2017-06-29 17:28:18 +02:00
Pierre Courtieu
a784a51c2e More lemmas about environments. 2017-06-27 14:33:58 +02:00
Pierre Courtieu
140b3b33ef Merge branch 'master' of git+ssh://scm.forge.open-do.org//scmrepos/git/sparkformal/sparkformal 2017-06-26 18:44:14 +02:00