aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2016-06-27Add Unset Shrink Abstract/Obligations in Coq85Matthieu Sozeau
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
2016-06-16Remove unneded hints in NZGcdMatthieu Sozeau
2016-06-16setoid_rewrite: fix the Params resolution tacticMatthieu Sozeau
2016-06-16Typeclasses: stdlib fixes for new search algorithmMatthieu Sozeau
2016-06-16In NMake_gen, giving to tactic do_size a grammar rule which respects the levels.Hugo Herbelin
2016-06-16Adding option "Set Reversible Pattern Implicit" to Specif.v so that anHugo Herbelin
2016-06-16Changing rule for "*" in Operator_Properties so that, iterated, itHugo Herbelin
2016-06-08Officially discontinue the experimental coq build via ocamlbuildPierre Letouzey
2016-06-06Relying instead on the Coq85 inclusion!Hugo Herbelin
2016-06-06Mode "Bracketing Last Introduction Pattern" is on for 8.4Hugo Herbelin
2016-06-06Mode "Regular Subst Tactic" is on in 8.6.Hugo Herbelin
2016-06-06Merge remote-tracking branch 'github/pr/118' into trunkMaxime Dénès
2016-06-03Removing "intro" from the tactic AST.Pierre-Marie Pédrot
2016-05-20Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-14Removing unexcepted activation of option "Regular Subst Tactic", sinceHugo Herbelin
2016-05-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-04NPeano : improve compatibility for this deprecated file via compat notationsPierre Letouzey
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
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-05-02Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-27Revert "Changing rule for "*" in Operator_Properties so that, iterated, it"Hugo Herbelin
2016-04-27Revert "Adding option "Set Reversible Pattern Implicit" to Specif.v so that an"Hugo Herbelin
2016-04-27Revert "In NMake_gen, giving to tactic do_size a grammar rule which respects ...Hugo Herbelin
2016-04-27Revert "Temporary hack to compensate missing comma while re-printing tactic"Hugo Herbelin
2016-04-27Temporary hack to compensate missing comma while re-printing tacticHugo Herbelin
2016-04-27In NMake_gen, giving to tactic do_size a grammar rule which respects the levels.Hugo Herbelin
2016-04-27Adding option "Set Reversible Pattern Implicit" to Specif.v so that anHugo Herbelin
2016-04-27Changing rule for "*" in Operator_Properties so that, iterated, itHugo Herbelin
2016-04-25Fixing bug #4684: Singleton list notation unusable in 8.5pl1.Pierre-Marie Pédrot
2016-04-09Merge branch 'v8.5'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-04-04Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Matthieu Sozeau
2016-03-30Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-24Fix handling of arity of definitional classes.Matthieu Sozeau
2016-03-06Moving Eauto to a simple ML file.Pierre-Marie Pédrot
2016-03-04Making parentheses mandatory in tactic scopes.Pierre-Marie Pédrot
2016-02-26Qcabs : absolute value on normalized rational numbers QcPierre Letouzey
2016-02-26Qcanon : fix names of lemmas Qcle_alt & Qcge_alt (were Qle_alt & Qge_alt)Pierre Letouzey
2016-02-26Qcanon : implement some old suggestions by C. AugerPierre Letouzey
2016-02-23Moving tauto.ml4 to a proper ML file.Pierre-Marie Pédrot
2016-02-22Moving the Tauto tactic to proper Ltac.Pierre-Marie Pédrot
2016-02-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-19Fixing bug #4582: cannot override notation [ x ].Pierre-Marie Pédrot
2016-01-29Merge branch 'v8.5'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 19:13:14 +0000