aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2016-09-19Adding an "extensionality in H" tactic which applies functionalHugo Herbelin
2016-09-17Further "decide equality" tests on demand of Jason.Hugo Herbelin
2016-09-15Extending "contradiction" so that it recognizes statements such as "~x=x" or ...Hugo Herbelin
2016-09-12Refolding: disable in 8.4 compat file, documentMatthieu Sozeau
2016-09-09no-refold patchPaul Steckler
2016-09-02Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-08-31Fix bug #5043: [Admitted] lemmas pick up section variables.Pierre-Marie Pédrot
2016-08-19Merge remote-tracking branch 'origin/pr/246' into v8.6Matthieu Sozeau
2016-08-18Merge remote-tracking branch 'github/bug4978' into v8.6Matthieu Sozeau
2016-08-18Fix an occurrence of deprecated eqn syntax in stdlib.Maxime Dénès
2016-08-17Fix #4978: priorities of Equivalence instancesMatthieu Sozeau
2016-07-18Replacing deprecated Implicit Arguments in prelude.Maxime Dénès
2016-07-18Remove the swap tactic from the prelude.Maxime Dénès
2016-07-18Fix bug #4923: Warning: appcontext is deprecated.Pierre-Marie Pédrot
2016-07-13Typo.Hugo Herbelin
2016-07-08Typo in a comment of stdlib.Hugo Herbelin
2016-07-08Program: Move ProofIrrelevance to Subset.vMatthieu Sozeau
2016-07-07Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-06Merge remote-tracking branch 'github/pr/199' into v8.5Maxime Dénès
2016-07-06Fix #4793: Coq 8.6 should accept -compat 8.6Maxime 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-28Typeclasses: use once in by clause for typeclass eautoMatthieu Sozeau
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-09Unbreak singleton list-like notation (-compat 8.4)Jason Gross
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 01:48:54 +0000