aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2016-10-03Remove if_then_else. Use tryif instead.Théo Zimmermann
2016-08-31Fix bug #5043: [Admitted] lemmas pick up section variables.Pierre-Marie Pédrot
2016-07-13Typo.Hugo Herbelin
2016-07-06Merge remote-tracking branch 'github/pr/199' into v8.5Maxime Dénès
2016-07-05Move option_map notation upJason Gross
2016-07-05Restore option_map in FMapFactsJason Gross
2016-07-05Compat84: Don't mess with stdlib modulesJason Gross
2016-06-09Unbreak singleton list-like notation (-compat 8.4)Jason Gross
2016-05-14Removing unexcepted activation of option "Regular Subst Tactic", sinceHugo Herbelin
2016-05-04NPeano : improve compatibility for this deprecated file via compat notationsPierre Letouzey
2016-05-04Int.v: simplify Jason's commit 5b4e3acePierre Letouzey
2016-05-04Merge branch 'move-compat-notations' of https://github.com/JasonGross/coq int...Pierre Letouzey
2016-04-25Fixing bug #4684: Singleton list notation unusable in 8.5pl1.Pierre-Marie Pédrot
2016-04-08Added compatibility coercions from Specif.v which were present in Coq 8.4.Hugo Herbelin
2016-04-05Add -compat 8.4 econstructor tactics, and testsJason Gross
2016-04-05Fix bug #4656Jason Gross
2016-04-04Update Coq84.vJason Gross
2016-04-04Add compatibility Nonrecursive Elimination SchemesJason Gross
2016-03-24Fix handling of arity of definitional classes.Matthieu Sozeau
2016-02-19Fixing bug #4582: cannot override notation [ x ].Pierre-Marie Pédrot
2016-01-23Fix bug #4503: mixing universe polymorphic and monomorphicMatthieu Sozeau
2016-01-20Update copyright headers.Maxime Dénès
2016-01-13MMaps: remove it from final 8.5 release, since this new library isn't mature ...Pierre Letouzey
2015-12-31Put implicits back as in 8.4.Matthieu Sozeau
2015-12-29Move compatibility notations to their proper filesJason Gross
2015-12-15Proof using: do not clear unused section hyps automaticallyEnrico Tassi
2015-12-15Refine tactic now shelves unifiable holes.Pierre-Marie Pédrot
2015-12-14Moved proof_admitted to its own file, named "AdmitAxiom.v".Maxime Dénès
2015-12-10Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Hugo Herbelin
2015-12-07Fix some typos.Guillaume Melquiond
2015-11-27Univs: entirely disallow instantiation of polymorphic constants withMatthieu Sozeau
2015-11-03Update compatibility file for some of bug #4392Jason Gross
2015-10-14Fix some typos.Guillaume Melquiond
2015-10-13Fix some typos.Guillaume Melquiond
2015-10-07Remove the "exists" overrides from Program. (Fix bug #4360)Guillaume Melquiond
2015-10-07Univs: add Strict Universe Declaration option (on by default)Matthieu Sozeau
2015-10-02Remove Print Universe directive.Matthieu Sozeau
2015-10-02Universes: enforce Set <= i for all Type occurrences.Matthieu Sozeau
2015-09-30Add compatibility files (feature 4319)Jason Gross
2015-09-08Emphasizing that eta for vectors is an instance of caseS, as pointedHugo Herbelin
2015-09-08Minor modifications to WeakFanTheorem.Hugo Herbelin
2015-09-08Adding a proof of eta on Vector.t of non-zero size.Hugo Herbelin
2015-08-02Reverting 16 last commits, committed mistakenly using the wrong push command.Hugo Herbelin
2015-08-02Adding a notation { x & P } for { x : _ & P }.Hugo Herbelin
2015-07-31Remove some outdated files and fix permissions.Guillaume Melquiond
2015-06-12The "on_last_hyp" tactic now behaves as it should.Cyprien Mangin
2015-05-12List.nth_error directly produces Some/None instead of value/errorPierre Letouzey
2015-05-12Mark PreOrder as a consequence of Equivalence. (Fix bug #4213)Guillaume Melquiond
2015-05-01Giving to "subst" a more natural semantic (fixing #4214) by using allHugo Herbelin
2015-04-09Prove [map_ext] using [map_ext_in].Nickolai Zeldovich
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 16:09:38 +0000