aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-07-26Merge PR #8050: Cleanup VERNAC EXTENDMaxime Dénès
2018-07-26Merge PR #8122: Fix #8119: anomalies in vm_compute with let and evars.Maxime Dénès
2018-07-26Merge PR #7786: In "redundant clause" pattern-matching error, show also the ↵Pierre-Marie Pédrot
pattern (closes #7777)
2018-07-26Merge PR #8084: Properly disable native compilation when -native-compiler is ↵Maxime Dénès
unset.
2018-07-26Merge PR #7274: Avoiding introducing dependency on the indices of a term ↵Pierre-Marie Pédrot
which has no matching clauses.
2018-07-26Merge PR #8150: Fix static declaration of plugins in coqpp.Emilio Jesus Gallego Arias
2018-07-25Merge PR #7859: Remove himsg.pr_puniverses, use @{} for universe printing in ↵Pierre-Marie Pédrot
errors
2018-07-25Merge PR #8133: Fixes #8126: issue with notations and nested applicationsEmilio Jesus Gallego Arias
2018-07-25Merge PR #734: [travis] Also run coqchk on HoTTEmilio Jesus Gallego Arias
2018-07-25In "redundant clause" pattern-matching error, show also the pattern (#7777).Hugo Herbelin
This is particularly useful when the pattern is part of a disjunction. Maybe this could be improved though, not mentioning the pattern when there is no disjunction, but that would be more work.
2018-07-25Optimized dependencies for pattern-matching on only trivial patterns.Hugo Herbelin
If a term is matched only against variables, it will not introduce a "match" and thus, even if the term is of an inductive type, its indices will not be taken into account in the current algorithm (though one could imagine an algorithm which does an expansion specially in order to filter on indices). This allows to tell the unification not to use dependencies which the pattern-matching algorithm is not able to exploit in practice. See example in file 2733.v.
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-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-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-22Merge PR #8095: Improvements for the chapter 'Detailed examples of tactics' ↵Théo Zimmermann
of the Reference Manual.
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-21Merge PR #8072: Fixes for chapters 'Vernacular commands', 'Proof handling' ↵Théo Zimmermann
and 'Tactics' of the Reference Manual.
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
2018-07-20Improved chapter 'The tactic language' of the Reference Manual.Zeimer
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 19:51:00 +0000