aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
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-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
2016-05-04More toplevel value representation sharing.Pierre-Marie Pédrot
2016-05-04Moving the Val module to Geninterp.Pierre-Marie Pédrot
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-04Fix Haskell extraction for terms over 45 characters longNickolai Zeldovich
2016-05-04Handle primitive projections inside types when extracting (bug #4616).Guillaume Melquiond
2016-05-04Merge branch 'haskell-type-indent' of https://github.com/zeldovich/coq into t...Pierre Letouzey
2016-05-03Remove extraneous space in coqtop/pg output (bug #4675).Guillaume Melquiond
2016-04-27Revert "Fixing printers for pr_auto_using and pr_firstorder_using."Hugo Herbelin
2016-04-27Revert "Fixing printing of Function."Hugo Herbelin
2016-04-27Revert "Adding printers for ring and field commands."Hugo Herbelin
2016-04-27Revert "Fixing a mispelling coma -> comma."Hugo Herbelin
2016-04-27Fixing a mispelling coma -> comma.Hugo Herbelin
2016-04-27Adding printers for ring and field commands.Hugo Herbelin
2016-04-27Fixing printing of Function.Hugo Herbelin
2016-04-27Fixing printers for pr_auto_using and pr_firstorder_using.Hugo Herbelin
2016-04-24Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-18Bugfix micromega: more careful syntaxification of terms of the form (Rinv t)Frédéric Besson
2016-04-12Removing redundant *_TYPED AS clauses in EXTEND statements.Pierre-Marie Pédrot
2016-04-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-09Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.vNickolai Zeldovich
2016-04-08Fixing a source of inefficiency and an artificial dependency in theDaniel de Rauglaudre
2016-04-01Getting rid of the "_mods" parsing entry.Pierre-Marie Pédrot
2016-03-19Moving the proof mode parsing management to Pcoq.Pierre-Marie Pédrot
2016-03-17Removing the special status of generic arguments defined by Coq itself.Pierre-Marie Pédrot
2016-03-17Removing the special status of generic entries defined by Coq itself.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 06:50:44 +0000