aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* ssrmatching: giving proper credits to the original author(s)Gravatar Enrico Tassi2016-06-15
* ssrmatching: ltac argument parsing made more robustGravatar Enrico Tassi2016-06-15
* ssrmatching: debug prints sent via msg_debugGravatar Enrico Tassi2016-06-15
* Rename "Set SsrMatchingDebug" into "Set Debug SsrMatching"Gravatar Enrico Tassi2016-06-15
* port ssrmatching plugin to the new makefileGravatar Enrico Tassi2016-06-14
* Merge remote-tracking branch 'origin/pr/146' into trunkGravatar Enrico Tassi2016-06-14
|\
* \ Merge remote-tracking branch 'origin/pr/173' into trunkGravatar Enrico Tassi2016-06-14
|\ \
* \ \ Merge remote-tracking branch 'github/evarunsafe' into trunkGravatar Matthieu Sozeau2016-06-14
|\ \ \
| * | | newring: fix for hack using evars as integers.Gravatar Matthieu Sozeau2016-06-09
* | | | Compilation via pack for plugins of the stdlibGravatar Pierre Letouzey2016-06-08
|/ / /
* | | Officially discontinue the experimental coq build via ocamlbuildGravatar Pierre Letouzey2016-06-08
| * | STM: proof block detection/error resilience APIGravatar Enrico Tassi2016-06-06
|/ /
* | Removing "intro" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* | A slight phase of documentation and uniformization of names ofGravatar Hugo Herbelin2016-06-02
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-01
|\ \
* | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| * | Extraction : add a location in the error message about polypropGravatar Pierre Letouzey2016-05-30
* | | Extraction : add a location in the error message about polypropGravatar Pierre Letouzey2016-05-30
| * | Extraction/Projections: Fix bug #4710Gravatar Matthieu Sozeau2016-05-23
| * | Disable memoization rather than failing when files cannot be opened.Gravatar Guillaume Melquiond2016-05-20
* | | Extraction: code cleanup in CommonGravatar Pierre Letouzey2016-05-20
| * | Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Gravatar Pierre Letouzey2016-05-19
* | | Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Gravatar Pierre Letouzey2016-05-19
* | | Micromega: qualify Coq.micromega.Tauto (avoid coqdep warnings about new Init/...Gravatar Pierre Letouzey2016-05-19
* | | Removing the old refine tactic from the Tactics module.Gravatar Pierre-Marie Pédrot2016-05-17
* | | Put the "generalize" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | | Put the "exact" family of tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | | Put the "fix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | | Put the "clear" tactic into the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* | | Interpretation function can return any untyped value.Gravatar Pierre-Marie Pédrot2016-05-04
* | | More toplevel value representation sharing.Gravatar Pierre-Marie Pédrot2016-05-04
* | | Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\| |
| * | Fix Haskell extraction for terms over 45 characters longGravatar Nickolai Zeldovich2016-05-04
| * | Handle primitive projections inside types when extracting (bug #4616).Gravatar Guillaume Melquiond2016-05-04
* | | Merge branch 'haskell-type-indent' of https://github.com/zeldovich/coq into t...Gravatar Pierre Letouzey2016-05-04
|\ \ \
| | * | Remove extraneous space in coqtop/pg output (bug #4675).Gravatar Guillaume Melquiond2016-05-03
* | | | Revert "Fixing printers for pr_auto_using and pr_firstorder_using."Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Fixing printing of Function."Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Adding printers for ring and field commands."Gravatar Hugo Herbelin2016-04-27
* | | | Revert "Fixing a mispelling coma -> comma."Gravatar Hugo Herbelin2016-04-27
* | | | Fixing a mispelling coma -> comma.Gravatar Hugo Herbelin2016-04-27
* | | | Adding printers for ring and field commands.Gravatar Hugo Herbelin2016-04-27
* | | | Fixing printing of Function.Gravatar Hugo Herbelin2016-04-27
* | | | Fixing printers for pr_auto_using and pr_firstorder_using.Gravatar Hugo Herbelin2016-04-27
* | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-24
|\ \ \ \ | | |/ / | |/| |
* | | | Bugfix micromega: more careful syntaxification of terms of the form (Rinv t)Gravatar Frédéric Besson2016-04-18
* | | | Removing redundant *_TYPED AS clauses in EXTEND statements.Gravatar Pierre-Marie Pédrot2016-04-12
* | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-09
|\ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-31 00:16:45 +0000