aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Program
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Remove most uses of function extensionality in Program.CombinatorsGravatar Jasper Hugunin2017-12-09
* Ensuring all .v files end with a newline to make "sed -i" work better on them.Gravatar Hugo Herbelin2017-08-21
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
* drop vo.itarget files and compute the corresponding the corresponding values ...Gravatar Matej Kosik2017-06-01
* Merge remote-tracking branch 'origin/pr/246' into v8.6Gravatar Matthieu Sozeau2016-08-19
|\
* | Fix bug #4923: Warning: appcontext is deprecated.Gravatar Pierre-Marie Pédrot2016-07-18
| * Program: Move ProofIrrelevance to Subset.vGravatar Matthieu Sozeau2016-07-08
|/
* Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
* Making parentheses mandatory in tactic scopes.Gravatar Pierre-Marie Pédrot2016-03-04
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-08
|\|
| * Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* | Experimenting removing strong normalization of the mid-statement in tactic cut.Gravatar Hugo Herbelin2015-12-05
|/
* Remove the "exists" overrides from Program. (Fix bug #4360)Gravatar Guillaume Melquiond2015-10-07
* The "on_last_hyp" tactic now behaves as it should.Gravatar Cyprien Mangin2015-06-12
* Revert "Fixing bug #4035 (support for dependent destruction within ltac code)."Gravatar Maxime Dénès2015-02-26
* Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23
* Fixing bug #4035 (support for dependent destruction within ltac code).Gravatar Hugo Herbelin2015-02-16
* dependent destruction: Fix (part of) bug #3961, by fixing dependent *Gravatar Matthieu Sozeau2015-02-14
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
* Update headers.Gravatar Maxime Dénès2015-01-12
* Forbid Require inside interactive modules and module types.Gravatar Maxime Dénès2014-12-25
* Add some missing Proof statements.Gravatar Guillaume Melquiond2014-09-17
* Make standard library independent of the names generated byGravatar Hugo Herbelin2014-06-04
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Ltac repeat is in fact already doing progressGravatar letouzey2012-10-01
* Updating headers.Gravatar herbelin2012-08-08
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Fix bug #2695: infinite loop in dependent destruction.Gravatar msozeau2012-06-19
* Final part of moving Program code inside the main code. Adapted add_definitio...Gravatar msozeau2012-03-14
* Fix unblocking code in dependent destruction due to zeta being used in unfold...Gravatar msozeau2012-02-01
* Fix simplification of ind. hyps., recognized by a [block] in their type (bug ...Gravatar msozeau2012-01-28
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* Fix bug #2456 and wrong unfolding of lets in the goal due to [unfold] doing z...Gravatar msozeau2011-10-17
* Avoid registering λ and Π as keywords just for some private Local NotationGravatar letouzey2011-09-06
* Making printing of backtick in Program reparsable (avoiding collision with "`(")Gravatar herbelin2011-06-14
* Fixed bug #2398: destruct ex2/sig2/sigT2 in Program, patch by Paolo Herms.Gravatar msozeau2011-06-07
* A module out of Program to have list notations (bug 2463)Gravatar pboutill2011-04-08
* Add a flag to hide obligations in Program-generated terms under anGravatar msozeau2011-02-28
* In Program obligation, do not use auto on non-proposition goals byGravatar msozeau2011-02-17
* First release of Vector library.Gravatar pboutill2010-12-10
* Used multiple lists of implicit arguments to transfer the choices ofGravatar herbelin2010-10-23
* Using multiple lists of implicit arguments in Program for preservingGravatar herbelin2010-10-03
* Fixed commit r13359 which was incomplete for its "trunk" part. ThanksGravatar herbelin2010-07-31
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 10:36:12 +0000