aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Collapse)Author
2016-05-20Disable memoization rather than failing when files cannot be opened.Guillaume Melquiond
Anomaly: Uncaught exception Unix.Unix_error(Unix.EACCES, "open", "lia.cache"). Please report.
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 ↵Pierre Letouzey
Init/Tauto.v)
2016-05-17Removing the old refine tactic from the Tactics module.Pierre-Marie Pédrot
It is indeed confusing, as it has little to do with the proper refine defined in the New submodule. Legacy code relying on it should call the Logic or Tacmach modules instead.
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
The Haskell extraction code would allow line-wrapping of the Haskell type definition, which would lead to unparseable Haskell code when the linebreak occured just before the type name. In particular, with a term name of 46 characters or more, the following Coq code: Definition xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx := tt. Extraction Language Haskell. Extraction xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx. would produce: xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx :: Unit xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx = Tt which failed to compile with GHC (according to Haskell's indentation rules, the "Unit" line must be indented to be treated as a continuation of the previous line). This patch always forces the type onto a separate line, and ensures that it is always indented by 2 spaces (just like the body of each definition).
2016-05-04Handle primitive projections inside types when extracting (bug #4616).Guillaume Melquiond
Note that extracting terms containing primitive projections is still utterly broken, so don't use them.
2016-05-04Merge branch 'haskell-type-indent' of https://github.com/zeldovich/coq into ↵Pierre Letouzey
trunk
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
This reverts commit 23ebfc41fba48ccce9bc878de258d1b0901f7dda.
2016-04-27Revert "Fixing printing of Function."Hugo Herbelin
This reverts commit cb6f036b8e097085a849f806aa7c2627b789bd1f.
2016-04-27Revert "Adding printers for ring and field commands."Hugo Herbelin
This reverts commit 9df1a3cf26d78df507d0e35c2d9ca987151777be.
2016-04-27Revert "Fixing a mispelling coma -> comma."Hugo Herbelin
This reverts commit 857dc0aaae30805725da213b6550dc1ff3a7adb2.
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
Bug uncovered by ekcburak@hotmail.com https://sympa.inria.fr/sympa/arc/coq-club/2016-04/msg00006.html Now, terms of the the form (Rinv t) are only syntaxified when t evaluates to a non-zero constant.
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
The extraction of [Z] into Ocaml's [Big_int] passed arguments in the wrong order to [Big.compare_case] for [Pos.compare_cont]. It seems unlikely this ever worked before.
2016-04-08Fixing a source of inefficiency and an artificial dependency in theDaniel de Rauglaudre
printer in the congruence tactic. Debugging messages were always built even when not in the verbose mode of congruence.
2016-04-01Getting rid of the "_mods" parsing entry.Pierre-Marie Pédrot
It was only used by setoid_ring for the Add Ring command, and was easily replaced by a dedicated argument. Moreover, it was of no use to tactic notations.
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
This makes the TACTIC EXTEND macro insensitive to Coq-defined arguments. They now have to be reachable in the ML code. Note that this has some consequences, as the previous macro was potentially mixing grammar entries and arguments as long as their name was the same. Now, each genarg comes with its grammar instead, so there is no way to abuse the macro.
2016-03-17Removing the special status of generic entries defined by Coq itself.Pierre-Marie Pédrot
The ARGUMENT EXTEND macro was discriminating between parsing entries known statically, i.e. defined in Pcoq and unknown entires. Although simplifying a bit the life of the plugin writer, it made actual interpretation difficult to predict and complicated the code of the ARGUMENT EXTEND macro. After this patch, all parsing entries and generic arguments used in an ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding a few more "open Pcoq.X" and "open Constrarg" here and there.
2016-03-17Adding a universe argument to Pcoq.create_generic_entry.Pierre-Marie Pédrot
2016-03-17Removing the registering of default values for generic arguments.Pierre-Marie Pédrot
2016-03-13Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Hugo Herbelin
2016-03-10Removing OCaml deprecated function names from the Lazy module.Pierre-Marie Pédrot
2016-03-06Removing useless grammar.cma dependencies.Pierre-Marie Pédrot
2016-03-06Splitting the nsatz ML module into an implementation and a grammar files.Pierre-Marie Pédrot
2016-03-06Moving Eauto to a simple ML file.Pierre-Marie Pédrot
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-05Using build_selector from Equality as a replacement of the selectorHugo Herbelin
in cctac which does not support indices properly. Incidentally, this should fix a failure in RelationAlgebra, where making prod_applist more robust (e8c47b652) revealed the discriminate bug in congruence.
2016-03-04Rename Ephemeron -> CEphemeron.Maxime Dénès
Fixes compilation of Coq with OCaml 4.03 beta 1.
2016-03-04Making parentheses mandatory in tactic scopes.Pierre-Marie Pédrot
2016-03-02Ssreflect pattern matching facilitiesEnrico Tassi
2016-02-24Getting rid of the "<:tactic< ... >>" quotations.Pierre-Marie Pédrot
It used to allow to represent parts of tactic AST directly in ML code. Most of the uses were trivial, only calling a constant, except for tauto that had an important code base written in this style. Removing this reduces the dependency to CAMLPX and the preeminence of Ltac in ML code.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 16:07:11 +0000