aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-07-26Expose the diff printing option as an UI entry in CoqIDE.Pierre-Marie Pédrot
2018-07-26Do not set diff printing on by default in CoqIDE.Pierre-Marie Pédrot
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-25Remove object duplication for Constraint command.Gaëtan Gilbert
2018-07-25Hints use Declare to declare universes instead of a custom object.Gaëtan Gilbert
2018-07-25Merge PR #7859: Remove himsg.pr_puniverses, use @{} for universe printing in ↵Pierre-Marie Pédrot
errors
2018-07-25Fix #7900 previous commit fixes a bug when using side effects in obligations.Matthieu Sozeau
Internal lemmas are inlined in obligations bodies, hence their universes have to be declared with the obligations themselves. ~sideff:true was not including the side effects universes and constraints in that case.
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-25[sphinx] Add a way of skipping names in the indexes.Théo Zimmermann
2018-07-25kernel: missing check that all universes are declared.Matthieu Sozeau
Keep the universe_levels_of_constr function inside typeops, not exported.
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-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)
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-29 09:34:46 +0000