aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init
Commit message (Expand)AuthorAge
...
| * | | | Add η principles for sigma typesGravatar Jason Gross2017-03-01
| * | | | Remove some trailing whitespace in Init/Specif.vGravatar Jason Gross2017-03-01
|/ / / /
| | | * Fixing a little bug in printing ex2 (type was printed "_" by default).Gravatar Hugo Herbelin2017-02-23
| * | | Allow interactive editing of Coq.Init.LogicGravatar Jason Gross2017-02-21
|/ / /
* / / Ltac as a plugin.Gravatar Pierre-Marie Pédrot2017-02-17
|/ /
* | Remove v62 from stdlib.Gravatar Théo Zimmermann2016-10-24
* | Replacing deprecated Implicit Arguments in prelude.Gravatar Maxime Dénès2016-07-18
* | Remove the swap tactic from the prelude.Gravatar Maxime Dénès2016-07-18
* | Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
* | Adding option "Set Reversible Pattern Implicit" to Specif.v so that anGravatar Hugo Herbelin2016-06-16
* | Revert "Adding option "Set Reversible Pattern Implicit" to Specif.v so that an"Gravatar Hugo Herbelin2016-04-27
* | Adding option "Set Reversible Pattern Implicit" to Specif.v so that anGravatar Hugo Herbelin2016-04-27
* | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Gravatar Matthieu Sozeau2016-04-04
|\ \
* | | Moving Eauto to a simple ML file.Gravatar Pierre-Marie Pédrot2016-03-06
* | | Moving tauto.ml4 to a proper ML file.Gravatar Pierre-Marie Pédrot2016-02-23
* | | Moving the Tauto tactic to proper Ltac.Gravatar Pierre-Marie Pédrot2016-02-22
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\ \ \ | | |/ | |/|
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | | Removing auto from the tactic AST.Gravatar Pierre-Marie Pédrot2015-12-24
| * | Remove Print Universe directive.Gravatar Matthieu Sozeau2015-10-02
| * | Universes: enforce Set <= i for all Type occurrences.Gravatar Matthieu Sozeau2015-10-02
| | * Move type_scope into user space, fix some output logsGravatar Jason Gross2015-08-14
| | * Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080Gravatar Jason Gross2015-08-14
| |/ |/|
| * Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
| * Adding a notation { x & P } for { x : _ & P }.Gravatar Hugo Herbelin2015-08-02
* | Tentatively setting cons and Some with 1st implicit argument maximalGravatar Hugo Herbelin2015-05-09
|/
* Fix various typos in documentationGravatar Matěj Grabovský2015-03-31
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Reorder the steps of the easy tactic. (Fix for bug #2630)Gravatar Guillaume Melquiond2015-02-25
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
* Update headers.Gravatar Maxime Dénès2015-01-12
* Improving elimination with indices, getting rid of intrusive residualGravatar Hugo Herbelin2014-11-02
* Supporting "at occs" as a short-hand for "in |- * at occs" in "destruct".Gravatar Hugo Herbelin2014-11-02
* eta contractionsGravatar Pierre Boutillier2014-10-01
* - Fix printing and parsing of primitive projections, including the SetGravatar Matthieu Sozeau2014-09-09
* Removing the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Instead of relying on a trick to make the constructor tactic parse, putGravatar Pierre-Marie Pédrot2014-08-07
* Removing the "constructor" tactic from the AST.Gravatar Pierre-Marie Pédrot2014-08-07
* Experimentally adding an option for automatically erasing anGravatar Hugo Herbelin2014-08-05
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
* Basic lemmas about the algebraic structure of equality.Gravatar Hugo Herbelin2014-05-31
* Moving argument-free tactics out of the AST into a dedicatedGravatar Pierre-Marie Pédrot2014-05-16
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
* Removing comment outdated since eta holds in conversion rule (thisGravatar Hugo Herbelin2014-05-07
* Try a new way of handling template universe levelsGravatar Matthieu Sozeau2014-05-06
* - 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
* No more Coersion in Init.Gravatar Pierre Boutillier2014-04-10
* Define [projT3] and [proj3_sig]Gravatar Jason Gross2014-04-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 01:10:36 +0000