aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init
Commit message (Expand)AuthorAge
* Merge PR#455: Farewell decl_modeGravatar Maxime Dénès2017-04-06
|\
* \ Merge PR#442: Allow interactive editing of Coq.Init.LogicGravatar Maxime Dénès2017-03-17
|\ \
* \ \ Merge PR#451: Add η principles for sigma typesGravatar Maxime Dénès2017-03-17
|\ \ \
| | | * Farewell decl_modeGravatar Enrico Tassi2017-03-07
| |_|/ |/| |
* | | A couple of other useful properties about compare_cont.Gravatar Hugo Herbelin2017-03-03
* | | Compatibility of iff wrt not and imp.Gravatar Hugo Herbelin2017-03-03
| * | Add η principles for sigma typesGravatar Jason Gross2017-03-01
| * | Remove some trailing whitespace in Init/Specif.vGravatar Jason Gross2017-03-01
|/ /
| * 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 16:42:28 +0000