aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2016-06-27Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-27ssrmatching: avoid warnings about redundant typing clauses in ARGUMENT EXTENDPierre Letouzey
2016-06-27Adding ability to put any pattern in binders, prefixed by a quote.Daniel de Rauglaudre
2016-06-24Removing tactic compatibility layers in setoid_ring.Pierre-Marie Pédrot
2016-06-23Fix typo.Guillaume Melquiond
2016-06-18Reuse the typing_flags datatype for inductives.Pierre-Marie Pédrot
2016-06-18Moving the typing_flags to the environment.Pierre-Marie Pédrot
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
2016-06-18Adding eintros to respect the e- prefix policy.Hugo Herbelin
2016-06-16Factorizing the uses of Declareops.safe_flags.Pierre-Marie Pédrot
2016-06-16Fixing a mispelling coma -> comma.Hugo Herbelin
2016-06-16Adding printers for ring and field commands.Hugo Herbelin
2016-06-16Fixing printing of Function.Hugo Herbelin
2016-06-16Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Pierre-Marie Pédrot
2016-06-16Remove inappropriate comment.Maxime Dénès
2016-06-15Remove the syntax changes introduced by this branch.Pierre-Marie Pédrot
2016-06-15ssrmatching: giving proper credits to the original author(s)Enrico Tassi
2016-06-15ssrmatching: ltac argument parsing made more robustEnrico Tassi
2016-06-15ssrmatching: debug prints sent via msg_debugEnrico Tassi
2016-06-15Rename "Set SsrMatchingDebug" into "Set Debug SsrMatching"Enrico Tassi
2016-06-14Assume totality: dedicated type rather than boolArnaud Spiwack
2016-06-14port ssrmatching plugin to the new makefileEnrico Tassi
2016-06-14Merge remote-tracking branch 'origin/pr/146' into trunkEnrico Tassi
2016-06-14Merge branch 'bug4725' into v8.5Matthieu Sozeau
2016-06-14Merge remote-tracking branch 'origin/pr/173' into trunkEnrico Tassi
2016-06-14Merge remote-tracking branch 'github/evarunsafe' into trunkMatthieu Sozeau
2016-06-09newring: fix for hack using evars as integers.Matthieu Sozeau
2016-06-08Compilation via pack for plugins of the stdlibPierre Letouzey
2016-06-08Officially discontinue the experimental coq build via ocamlbuildPierre Letouzey
2016-06-06STM: proof block detection/error resilience APIEnrico Tassi
2016-06-03Removing "intro" from the tactic AST.Pierre-Marie Pédrot
2016-06-02A slight phase of documentation and uniformization of names ofHugo Herbelin
2016-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-30Extraction : add a location in the error message about polypropPierre Letouzey
2016-05-30Extraction : add a location in the error message about polypropPierre Letouzey
2016-05-26Univs/Program/Function: Fix bug #4725Matthieu Sozeau
2016-05-23Extraction/Projections: Fix bug #4710Matthieu Sozeau
2016-05-20Disable memoization rather than failing when files cannot be opened.Guillaume Melquiond
2016-05-20Extraction: code cleanup in CommonPierre Letouzey
2016-05-19Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Pierre Letouzey
2016-05-19Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Pierre Letouzey
2016-05-19Micromega: qualify Coq.micromega.Tauto (avoid coqdep warnings about new Init/...Pierre Letouzey
2016-05-17Removing the old refine tactic from the Tactics module.Pierre-Marie Pédrot
2016-05-16Put the "generalize" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "exact" family of tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "fix" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "clear" tactic into the monad.Pierre-Marie Pédrot
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-04Interpretation function can return any untyped value.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 04:59:14 +0000