aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Collapse)AuthorAge
...
* | Fixing printing of Function.Gravatar Hugo Herbelin2016-06-16
| |
* | Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \
* | | Remove inappropriate comment.Gravatar Maxime Dénès2016-06-16
| | |
| * | Remove the syntax changes introduced by this branch.Gravatar Pierre-Marie Pédrot2016-06-15
| | | | | | | | | | | | | | | | | | We decided to only export the API, so that an external plugin can provide this feature without having to merge it in current Coq trunk. This postpones the attribute implementation in vernacular commands after 8.6.
* | | ssrmatching: giving proper credits to the original author(s)Gravatar Enrico Tassi2016-06-15
| | | | | | | | | | | | | | | Following CeCILL-B 5.3.2, we are allowed to redistribute the software under the same license of Coq as long as we credit.
* | | 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
| | | | | | | | | | | | for uniformity with other Debug options.
| * | Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
| | | | | | | | | | | | | | | | | | | | | The rational is that 1. further typing flags may be available in the future 2. it makes it easier to trace and document the argument
* | | port ssrmatching plugin to the new makefileGravatar Enrico Tassi2016-06-14
| | |
* | | Merge remote-tracking branch 'origin/pr/146' into trunkGravatar Enrico Tassi2016-06-14
|\ \ \ | | | | | | | | | | | | | | | | Conflicts: Makefile.common
| | | * Merge branch 'bug4725' into v8.5Gravatar Matthieu Sozeau2016-06-14
| | | |\
* | | | \ Merge remote-tracking branch 'origin/pr/173' into trunkGravatar Enrico Tassi2016-06-14
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | This is the "error resiliency" mode for STM
* \ \ \ \ \ 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
|/ / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | For now, the pack name reuse the previous .cma name of the plugin, (extraction_plugin, etc). The earlier .mllib files in plugins are now named .mlpack. They are also handled by bin/ocamllibdep, just as .mllib. We've slightly modified ocamllibdep to help setting the -for-pack options: in *.mlpack.d files, there are some extra variables such as foo/bar_FORPACK := -for-pack Baz when foo/bar.ml is mentioned in baz.mlpack. When a plugin is calling a function from another plugin, the name need to be qualified (Foo_plugin.Bar.baz instead of Bar.baz). Btw, we discard the generated files plugins/*/*_mod.ml, they are obsolete now, replaced by DECLARE PLUGIN. Nota: there's a potential problem in the micromega directory, some .ml files are linked both in micromega_plugin and in csdpcert. And we now compile these files with a -for-pack, even if they are not packed in the case of csdpcert. In practice, csdpcert seems to work well, but we should verify with OCaml experts.
* | | | | | Officially discontinue the experimental coq build via ocamlbuildGravatar Pierre Letouzey2016-06-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It has been accidentaly broken since early 2014 (and especially in 8.5), no easy repair, I won't devote any more hours to this stuff. Moreover no one seems to care apart from Emilio, but he's ok to work on this in a separate repository or branch. I left a dev/doc/ocamlbuild.txt file with a few words about this experiment.
| * | | | | STM: proof block detection/error resilience APIGravatar Enrico Tassi2016-06-06
|/ / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit introduces the concept of proof blocks that are resilient to errors. They are represented as ErrorBound boxes in the STM document with the topological invariant that they never overlap. The detection and error recovery of ErrorBound boxes is defined outside the STM. One can define a box by providing a function to detect it statically by crawling the parsed document and a function to recover from an error at run time.
* | | | | Removing "intro" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Note that this breaks the compatibility, in a beneficial way I believe. Tactics defined in strict mode (i.e. through Ltac foo := ...) may not do an introduction on a local identifier anymore. They must use the "fresh" primitive instead.
* | | | | A slight phase of documentation and uniformization of names ofGravatar Hugo Herbelin2016-06-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | functions about interpretation, internalization, externalization of notations. Main syntactic changes: - subst_aconstr_in_glob_constr -> instantiate_notation_constr (because aconstr has been renamed to notation_constr long time ago) - extern_symbol -> extern_notation (because symbol.ml has been renamed to notation.ml long time ago) - documentation of notations_ops.mli Main semantic changes: - Notation_ops.eq_glob_constr which was partial eq disappears: use glob_constr_eq instead - In particular, this impacts a change on funind which now use the (fully implemented) glob_constr_eq Somehow, instantiate_notation_constr should be in notation_ops.ml for symmetry with match_notation_constr but it is bit painful to do.
* | | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-01
|\ \ \ \ \ | | |_|/ / | |/| | |
* | | | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
| * | | | 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
| | | | |
| | | | * Univs/Program/Function: Fix bug #4725Gravatar Matthieu Sozeau2016-05-26
| | |_|/ | |/| | | | | | | | | | | | | | | | | | | | | | - In Program, a check_evars_are_solved was introduced too early. Program does it's checking of evars by itself. - In Function, the universe environments were not threaded correctly.
| * | | Extraction/Projections: Fix bug #4710Gravatar Matthieu Sozeau2016-05-23
| | | | | | | | | | | | | | | | | | | | Use the compatibility match construction to extract the compatibility constant associated to a primitive projection.
| * | | Disable memoization rather than failing when files cannot be opened.Gravatar Guillaume Melquiond2016-05-20
| | | | | | | | | | | | | | | | | | | | Anomaly: Uncaught exception Unix.Unix_error(Unix.EACCES, "open", "lia.cache"). Please report.
* | | | 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 ↵Gravatar Pierre Letouzey2016-05-19
| | | | | | | | | | | | | | | | Init/Tauto.v)
* | | | Removing the old refine tactic from the Tactics module.Gravatar Pierre-Marie Pédrot2016-05-17
| | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | 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
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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).
| * | | Handle primitive projections inside types when extracting (bug #4616).Gravatar Guillaume Melquiond2016-05-04
| | | | | | | | | | | | | | | | | | | | Note that extracting terms containing primitive projections is still utterly broken, so don't use them.
* | | | Merge branch 'haskell-type-indent' of https://github.com/zeldovich/coq into ↵Gravatar Pierre Letouzey2016-05-04
|\ \ \ \ | | | | | | | | | | | | | | | trunk
| | * | | 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
| | | | | | | | | | | | | | | | | | | | This reverts commit 23ebfc41fba48ccce9bc878de258d1b0901f7dda.
* | | | | Revert "Fixing printing of Function."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | | | | | This reverts commit cb6f036b8e097085a849f806aa7c2627b789bd1f.
* | | | | Revert "Adding printers for ring and field commands."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | | | | | This reverts commit 9df1a3cf26d78df507d0e35c2d9ca987151777be.
* | | | | Revert "Fixing a mispelling coma -> comma."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | | | | | This reverts commit 857dc0aaae30805725da213b6550dc1ff3a7adb2.
* | | | | Fixing a mispelling coma -> comma.Gravatar Hugo Herbelin2016-04-27
| | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 02:30:34 +0000