aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Officially discontinue the experimental coq build via ocamlbuildGravatar Pierre Letouzey2016-06-08
* 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
|\ \ \
| | * | Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.vGravatar Nickolai Zeldovich2016-04-09
| |/ /
| * | Fixing a source of inefficiency and an artificial dependency in theGravatar Daniel de Rauglaudre2016-04-08
* | | Getting rid of the "_mods" parsing entry.Gravatar Pierre-Marie Pédrot2016-04-01
* | | Moving the proof mode parsing management to Pcoq.Gravatar Pierre-Marie Pédrot2016-03-19
* | | Removing the special status of generic arguments defined by Coq itself.Gravatar Pierre-Marie Pédrot2016-03-17
* | | Removing the special status of generic entries defined by Coq itself.Gravatar Pierre-Marie Pédrot2016-03-17
* | | Adding a universe argument to Pcoq.create_generic_entry.Gravatar Pierre-Marie Pédrot2016-03-17
* | | Removing the registering of default values for generic arguments.Gravatar Pierre-Marie Pédrot2016-03-17
* | | Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Gravatar Hugo Herbelin2016-03-13
* | | Removing OCaml deprecated function names from the Lazy module.Gravatar Pierre-Marie Pédrot2016-03-10
* | | Removing useless grammar.cma dependencies.Gravatar Pierre-Marie Pédrot2016-03-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 22:18:52 +0000