aboutsummaryrefslogtreecommitdiffstats
path: root/common/Smallstep.v
Commit message (Expand)AuthorAgeFilesLines
* Adapt to coq/coq#13837 ("apply with" does not rename arguments) (#417)Gaëtan Gilbert2021-10-031-1/+1
* Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-4/+5
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-10/+10
* Additional simulation diagrams for determinate source languagesXavier Leroy2019-06-061-0/+173
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-3/+3
* Put forward_simulation and backward_simulation in Prop instead of TypeXavier Leroy2016-03-061-255/+275
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-175/+175
* Make small-step semantics more parametric w.r.t. the type of global environme...Xavier Leroy2014-11-261-22/+37
* Add Genv.public_symbol operation.Xavier Leroy2014-11-241-14/+14
* Remove some useless "Require".xleroy2012-12-301-1/+0
* Merge of the "volatile" branch:xleroy2012-02-041-28/+275
* Merge of branch new-semantics: revised and strengthened top-level statements ...xleroy2011-07-151-457/+994
* Merge of branches/full-expr-4:xleroy2010-08-181-0/+50
* Existence of behaviorsxleroy2010-01-311-2/+126
* Distinguish two kinds of nonterminating behaviors: silent divergencexleroy2009-08-161-25/+262
* Added 'going wrong' behaviorsxleroy2009-08-051-11/+34
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-8/+8
* Fusion partielle de la branche contsem: xleroy2008-07-081-54/+123
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+15
* Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les express...xleroy2007-08-281-13/+18
* Ajout de common/Complements.vxleroy2007-08-261-0/+10
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-0/+460
generated by cgit (git 2.34.1) at 2024-05-09 18:16:20 +0000