aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-07-27[ci] Remove CircleCI setup.Emilio Jesus Gallego Arias
GitLab setup is quite stable these days thanks to the work of many people and `coqbot`. We decided to keep CircleCI support for a while as a safeguard in case something happened in the migration to GitLab, but these days we are just wasting resources to them and to us. As I'm afraid CircleCI won't scale for us, the time to remove it has arrived. Still, CircleCI had some awesome functionality that GitLab's CI doesn't offer yet, see the links at: https://github.com/coq/coq/issues/6919#issuecomment-395885573 - https://gitlab.com/gitlab-org/gitlab-ce/issues/29347 - https://gitlab.com/gitlab-org/gitlab-ce/issues/35222 - https://gitlab.com/gitlab-org/gitlab-ce/issues/41947 - https://gitlab.com/gitlab-org/gitlab-ce/issues/47063
2018-07-27Merge PR #8164: Add information to option type errorsEnrico Tassi
2018-07-27Merge PR #8166: Fix Search query in CoqIDE.Enrico Tassi
2018-07-27Merge PR #8103: Coercions cleanup: use GlobRef.t instead of constrEnrico Tassi
2018-07-27Merge PR #8141: Diff option in CoqIDEEnrico Tassi
2018-07-26Merge PR #8101: Remove ClosedModule and ClosedSection from libstackEnrico Tassi
2018-07-26Fix Search query in CoqIDE.Pierre-Marie Pédrot
For some reason the code was just doing random stuff that did not make sense.
2018-07-26Add information to option type errorsTej Chajed
Print the expected and actual types for the option value (which is one of bool, int, or string).
2018-07-26Replace iter + ref by fold_leftMaxime Dénès
2018-07-26restore reduction of coercion to eventually expose a constructorEnrico Tassi
2018-07-26Coercions cleanup: use GlobRef.t instead of constrMaxime Dénès
2018-07-26Merge PR #8100: Use just one object declaration for all global universe ↵Pierre-Marie Pédrot
additions
2018-07-26Merge PR #8050: Cleanup VERNAC EXTENDMaxime Dénès
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-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.)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 07:04:03 +0000