aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Remove if_then_else. Use tryif instead.Gravatar Théo Zimmermann2016-10-03
* Fix bug #5043: [Admitted] lemmas pick up section variables.Gravatar Pierre-Marie Pédrot2016-08-31
* Typo.Gravatar Hugo Herbelin2016-07-13
* Merge remote-tracking branch 'github/pr/199' into v8.5Gravatar Maxime Dénès2016-07-06
|\
* | Move option_map notation upGravatar Jason Gross2016-07-05
* | Restore option_map in FMapFactsGravatar Jason Gross2016-07-05
| * Compat84: Don't mess with stdlib modulesGravatar Jason Gross2016-07-05
| * Unbreak singleton list-like notation (-compat 8.4)Gravatar Jason Gross2016-06-09
|/
* Removing unexcepted activation of option "Regular Subst Tactic", sinceGravatar Hugo Herbelin2016-05-14
* NPeano : improve compatibility for this deprecated file via compat notationsGravatar Pierre Letouzey2016-05-04
* Int.v: simplify Jason's commit 5b4e3aceGravatar Pierre Letouzey2016-05-04
* Merge branch 'move-compat-notations' of https://github.com/JasonGross/coq int...Gravatar Pierre Letouzey2016-05-04
|\
* | Fixing bug #4684: Singleton list notation unusable in 8.5pl1.Gravatar Pierre-Marie Pédrot2016-04-25
* | Added compatibility coercions from Specif.v which were present in Coq 8.4.Gravatar Hugo Herbelin2016-04-08
* | Add -compat 8.4 econstructor tactics, and testsGravatar Jason Gross2016-04-05
* | Fix bug #4656Gravatar Jason Gross2016-04-05
* | Update Coq84.vGravatar Jason Gross2016-04-04
* | Add compatibility Nonrecursive Elimination SchemesGravatar Jason Gross2016-04-04
* | Fix handling of arity of definitional classes.Gravatar Matthieu Sozeau2016-03-24
* | Fixing bug #4582: cannot override notation [ x ].Gravatar Pierre-Marie Pédrot2016-02-19
* | Fix bug #4503: mixing universe polymorphic and monomorphicGravatar Matthieu Sozeau2016-01-23
* | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | MMaps: remove it from final 8.5 release, since this new library isn't mature ...Gravatar Pierre Letouzey2016-01-13
* | Put implicits back as in 8.4.Gravatar Matthieu Sozeau2015-12-31
| * Move compatibility notations to their proper filesGravatar Jason Gross2015-12-29
|/
* Proof using: do not clear unused section hyps automaticallyGravatar Enrico Tassi2015-12-15
* Refine tactic now shelves unifiable holes.Gravatar Pierre-Marie Pédrot2015-12-15
* Moved proof_admitted to its own file, named "AdmitAxiom.v".Gravatar Maxime Dénès2015-12-14
* Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Gravatar Hugo Herbelin2015-12-10
* Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* Univs: entirely disallow instantiation of polymorphic constants withGravatar Matthieu Sozeau2015-11-27
* Update compatibility file for some of bug #4392Gravatar Jason Gross2015-11-03
* Fix some typos.Gravatar Guillaume Melquiond2015-10-14
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Remove the "exists" overrides from Program. (Fix bug #4360)Gravatar Guillaume Melquiond2015-10-07
* Univs: add Strict Universe Declaration option (on by default)Gravatar Matthieu Sozeau2015-10-07
* Remove Print Universe directive.Gravatar Matthieu Sozeau2015-10-02
* Universes: enforce Set <= i for all Type occurrences.Gravatar Matthieu Sozeau2015-10-02
* Add compatibility files (feature 4319)Gravatar Jason Gross2015-09-30
* Emphasizing that eta for vectors is an instance of caseS, as pointedGravatar Hugo Herbelin2015-09-08
* Minor modifications to WeakFanTheorem.Gravatar Hugo Herbelin2015-09-08
* Adding a proof of eta on Vector.t of non-zero size.Gravatar Hugo Herbelin2015-09-08
* 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
* Remove some outdated files and fix permissions.Gravatar Guillaume Melquiond2015-07-31
* The "on_last_hyp" tactic now behaves as it should.Gravatar Cyprien Mangin2015-06-12
* List.nth_error directly produces Some/None instead of value/errorGravatar Pierre Letouzey2015-05-12
* Mark PreOrder as a consequence of Equivalence. (Fix bug #4213)Gravatar Guillaume Melquiond2015-05-12
* Giving to "subst" a more natural semantic (fixing #4214) by using allGravatar Hugo Herbelin2015-05-01
* Prove [map_ext] using [map_ext_in].Gravatar Nickolai Zeldovich2015-04-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 07:48:15 +0000