aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-07-25Fix static declaration of plugins in coqpp.Pierre-Marie Pédrot
The module was not properly registered with dynlink turned off, leading to a failure of compilation of the prelude.
2018-07-25Doc: preliminary work before #7291 which add an "Unable to unify" message.Hugo Herbelin
We adopt the convention that error messages with a template use the sphinx syntax used in defining syntax rules.
2018-07-25[ssr] assertion -> error message (Fix #8134)Enrico Tassi
2018-07-25Add overlay for EquationsGaëtan Gilbert
2018-07-25Remove himsg.pr_puniverses, use @{} for universe printing in errorsMaxime Dénès
Replaces #6401.
2018-07-25Merge PR #7889: Cleanup reduction effects: they only work on constants.Pierre-Marie Pédrot
2018-07-25Merge PR #8139: Replace all the CoInductives with Variants in the SSR pluginEnrico Tassi
2018-07-25Merge PR #8063: Direct implementation of Ascii.eqb and String.eqb (take 2)Hugo Herbelin
2018-07-25Replace all the CoInductives with Variants in the SSR pluginKazuhiko Sakaguchi
2018-07-24[travis] Also run coqchk on HoTTJason Gross
2018-07-24Merge PR #7908: Projections use index representationPierre-Marie Pédrot
2018-07-24Fix #8119: anomalies in vm_compute with let and evars.Pierre-Marie Pédrot
There were actually two broken things with VM + evars, the fixes are: - Do not pass let-bound arguments to evars. - Use the right order for evar arguments. Native compilation seems to be suffering from the same shortcomings, I will open a separate bug and adapt the PR.
2018-07-24Add combinators to drop the bodies of local declarations.Pierre-Marie Pédrot
2018-07-24Properly disable native compilation when -native-compiler is unset.Pierre-Marie Pédrot
There was a function used by the pretyper that did not check that the flag was set, leading to native compilation even when the configure flag was off.
2018-07-24Merge PR #8040: [ci] Enable native compiler in `egde:flambda` build.Gaëtan Gilbert
2018-07-24Add simple test cases for vm and native on primitive projections.Gaëtan Gilbert
2018-07-24VM: don't duplicate projection narg information in lproj/kprojGaëtan Gilbert
2018-07-24Add overlay for Equations.Gaëtan Gilbert
2018-07-24Fix #7329: coqchk Include with primitive projectionsGaëtan Gilbert
2018-07-24Projections use index representationGaëtan Gilbert
The upper layers still need a mapping constant -> projection, which is provided by Recordops.
2018-07-24Fixes #8126 (issue with notations and nested applications).Hugo Herbelin
No reason not to collapse inner applications with explicit arguments. This is compatible with the ad hoc encoding of @f as GApp(f,[])/NApp(f,[]).
2018-07-24Remove useless is_projection in tacredGaëtan Gilbert
2018-07-24Move Heads to pretyping (is_projection will move to Recordops)Gaëtan Gilbert
2018-07-24Update the documentation w.r.t. the new error raised by unify.Pierre-Marie Pédrot
2018-07-24[ci] Enable native compiler in `egde:flambda` build.Emilio Jesus Gallego Arias
OCaml 4.07.0 should have fixed the (memory eating bug)[https://caml.inria.fr/mantis/view.php?id=7630]
2018-07-24Merge PR #6801: Highlight differences between successive proof steps (color, ↵Emilio Jesus Gallego Arias
underline, etc.)
2018-07-24Merge PR #8083: Add test for repeated section with same nameThéo Zimmermann
2018-07-24Merge PR #8000: Fix #7854: Native compilation + flambda trigger SEGFAULT.Maxime Dénès
2018-07-24Merge PR #6597: Binary, Octal, and Hex conversions between [positive], [Z], ↵Hugo Herbelin
[N], [nat] and [string]
2018-07-23Make tokenize_string an optional parameter for diff methods in pp_diffs.Jim Fehrle
Remove forward reference to lexer.
2018-07-23Displays the differences between successive proof steps in coqtop and CoqIDE.Jim Fehrle
Proof General requires minor changes to make the diffs visible, but this code shouldn't break the existing version of PG. Diffs are computed for the hypotheses and conclusion of the first goal between the old and new proofs. Strings are split into tokens using the Coq lexer, then the list of tokens are diffed using the Myers algorithm. A fixup routine (Pp_diff.shorten_diff_span) shortens the span of the diff result in some cases. Diffs can be enabled with the Coq commmand "Set Diffs on|off|removed." or "-diffs on|off|removed" on the OS command line. The "on" option shows only the new item with added text, while "removed" shows each modified item twice--once with the old value showing removed text and once with the new value showing added text. The highlights use 4 tags to specify the color and underline/strikeout. These are "diffs.added", "diffs.removed", "diffs.added.bg" and "diffs.removed.bg". The first two are for added or removed text; the last two are for unmodified parts of a modified item. Diffs that span multiple strings in the Pp are tagged with "start.diff.*" and "end.diff.*", but only on the first and last strings of the span.
2018-07-23Add test for repeated section with same nameJasper Hugunin
2018-07-23Make the out_channel for the log file accessible so tests can write to it ↵Jim Fehrle
(e.g. for debugging)
2018-07-23Generate more compact escape sequences byJim
a) not explicitly setting the default value and b) not repeating attributes that are already set. Example (omitting escape character): Old: E : [92;49;22;23;24;27mev[39;49;22;23;24;27m [39;49;22;23;24;27mn[39;49;22;23;24;27m New: E : [92mev[0m n (92 is bright green, the other codes set default attributes).
2018-07-23Adding environment-manipulating functions.Pierre-Marie Pédrot
2018-07-23Fix deprecated warnings from Pcoq.Pierre-Marie Pédrot
2018-07-23Merge remote-tracking branch 'origin/pr/54'Pierre-Marie Pédrot
2018-07-22Merge PR #8095: Improvements for the chapter 'Detailed examples of tactics' ↵Théo Zimmermann
of the Reference Manual.
2018-07-22Docs: minor typo in "Template Polymorphism"Timothy Bourke
2018-07-22Docs: minor typo in W-Ind relative to textTimothy Bourke
The rule uses s'_j, the text refers to s_j, the latter is simpler in the absence of any other constraints.
2018-07-21Solved problems with snippets giving errors in chapter 'Detailed examples of ↵Zeimer
tactics' of the Reference Manual. Refreshed the section on the cardinality of the naturals. Removed the mention of specialize_eqs as it seems very bugged.
2018-07-21Rewrote examples about permutations, logic and type isomorphisms: changed ↵Zeimer
the formatting and renamed the tactics to match modern naming conventions.
2018-07-21Improvements for the chapter 'Detailed examples of tactics' of the Reference ↵Zeimer
Manual.
2018-07-21Docs: Fix p values in CIC Inductive Defs examplesTimothy Bourke
It seems that p is a natural number, so why not write it as 0 rather than the empty list for tree and forest? And, if I understand correctly, odd and even have p = 0 and Arr(even) = Arr(odd) = 1.
2018-07-21Merge PR #8072: Fixes for chapters 'Vernacular commands', 'Proof handling' ↵Théo Zimmermann
and 'Tactics' of the Reference Manual.
2018-07-21Fixing capital letters in the "in" syntax of instantiate.Hugo Herbelin
This trace of V7 syntax remained unnoticed (since July 2004).
2018-07-21[doc] Fix grammar of goal selectors.Théo Zimmermann
2018-07-21A few Sphinx fixes in the Ltac chapter.Théo Zimmermann
Including using subscripts more often.
2018-07-21Merge PR #8086: Improved chapter 'The tactic language' of the Reference Manual.Théo Zimmermann
2018-07-20Small improvements suggested in comments to PR #8086.Zeimer
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 14:05:16 +0000