aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-05-28Add lemmas about equality of sigma typesJason Gross
2017-05-28Use [rew_] instead of [eq_rect_] prefixJason Gross
As per Hugo's request.
2017-05-28Use [rew] notations rather than [eq_rect]Jason Gross
As per Hugo's request in https://github.com/coq/coq/pull/384#issuecomment-264891011
2017-05-28Add more groupoid-like theorems about [eq]Jason Gross
2017-05-28Merge PR#679: Bug 5546, qualify datatype constructors when needed in Show MatchMaxime Dénès
2017-05-28Don't disable deprecation warning for configure.mlGaëtan Gilbert
2017-05-28Merge PR#684: Trunk+fix coq makefile test suite on nixosMaxime Dénès
2017-05-28Merge PR#681: Fix votour for safe strings & warningsMaxime Dénès
2017-05-28Gitlab CIGaëtan Gilbert
2017-05-28Merge PR#680: add Show test with -emacs flag for trunkMaxime Dénès
2017-05-28Merge PR#676: Primitive Ltac definitions for first and solveMaxime Dénès
2017-05-28Merge PR#658: [coqdoc] Add keywords in bug 2884.Maxime Dénès
2017-05-27[stm] Rename Side-Effect type.Emilio Jesus Gallego Arias
As suggested by @gares, now the meaning becomes way clearer.
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
This is the continuation of #244, we now deprecate `CErrors.error`, the single entry point in Coq is `user_err`. The rationale is to allow for easier grepping, and to ease a future cleanup of error messages. In particular, we would like to systematically classify all error messages raised by Coq and be sure they are properly documented. We restore the two functions removed in #244 to improve compatibility, but mark them deprecated.
2017-05-27[stm] Uniformize `Sideff / Sideff.Emilio Jesus Gallego Arias
This is a minor cleanup.
2017-05-27[coqlib] Move `Coqlib` to `library/`.Emilio Jesus Gallego Arias
We move Coqlib to library in preparation for the late binding of Gallina-level references. Placing `Coqlib` in `library/` is convenient as some components such as pretyping need to depend on it. By moving we lose the ability to locate references by syntactic abbreviations, but IMHO it makes to require ML code to refer to a true constant instead of an abbreviation/notation. Unfortunately this change means that we break the `Coqlib` API (providing a compatibility function is not possible), however we do so for a good reason. The main changes are: - move `Coqlib` to `library/`. - remove reference -> term from `Coqlib`. In particular, clients will have different needs with regards to universes/evar_maps, so we force them to call the (not very safe) `Universes.constr_of_global` explicitly so the users are marked. - move late binding of impossible case from `Termops` to `pretying/Evarconv`. Remove hook. - `Coqlib.find_reference` doesn't support syntactic abbreviations anymore. - remove duplication of `Coqlib` code in `Program`. - remove duplication of `Coqlib` code in `Ltac.Rewrite`. - A special note about bug 5066 and commit 6e87877 . This case illustrates the danger of duplication in the code base; the solution chosen there was to transform the not-found anomaly into an error message, however the general policy was far from clear. The long term solution is indeed make `find_reference` emit `Not_found` and let the client handle the error maybe non-fatally. (so they can test for constants.
2017-05-27[coqlib] Deprecate redundant Coqlib functions.Emilio Jesus Gallego Arias
We remove redundant functions `coq_constant`, `gen_reference`, and `gen_constant`. This is a first step towards a lazy binding of libraries references. We have also chosen to untangle `constr` from `Coqlib`, as how to instantiate the reference (in particular wrt universes) is a client-side issue. (The client may want to provide an `evar_map` ?) c.f. #186
2017-05-27coq_makefile: build .cma for each .mlpackEnrico Tassi
It used to generate only .cmo (the packed one). While this works if the plugin has no external dependencies, it does not if it does. The bug affected only bytecode builds
2017-05-27Documenting the existence of first and solve as Ltac definitions.Pierre-Marie Pédrot
2017-05-27Exporting a few primitive tacticals as named Ltac definitions.Pierre-Marie Pédrot
2017-05-27Merge PR#686: [travis] temporary UniMath overlayMaxime Dénès
2017-05-27[travis] temporary UniMath overlayMaxime Dénès
We are waiting for an upstream merge of a fix related to coq_makefile2.
2017-05-27Add execution permission to test-suite file.Théo Zimmermann
2017-05-27Use specific shell for more robustness.Théo Zimmermann
2017-05-27Fix test-suite/coq-makefile on NixOS.Théo Zimmermann
2017-05-26Changes to make coq-makefile not failing on MacOS X.Hugo Herbelin
There is still however a failure with "rmdir --ignore-fail-on-non-empty".
2017-05-26Merge pull request #7 from SkySkimmer/checker+fix_votourEmilio Jesús Gallego Arias
[checker] [votour] resolve warning 52 fragile constant pattern
2017-05-26[checker] [votour] resolve warning 52 fragile constant patternGaëtan Gilbert
Also stop using failwith for flow control in tuple_of_string.
2017-05-26Merge PR#666: romega revisited : no more normalization trace, cleaned-up ↵Maxime Dénès
resolution trace
2017-05-26Merge PR#634: Fix bug #5526, don't check for nonlinearity in notation if ↵Maxime Dénès
printing only
2017-05-26Merge PR#655: Extra functions exported in EConstrMaxime Dénès
2017-05-26[checker] Add bin/votour to the coqocaml target.Emilio Jesus Gallego Arias
2017-05-26[votour] Fix/disable warnings.Emilio Jesus Gallego Arias
2017-05-26[votour] Fix build with -safe-string (bug 5553)Emilio Jesus Gallego Arias
2017-05-26Merge PR#672: Add parsers-examples target to fiat-parsers ciMaxime Dénès
2017-05-25add Show test with -emacs flagPaul Steckler
2017-05-25Bug 5546, qualify datatype constructors when neededPaul Steckler
2017-05-25Merge PR#645: [stm] Tweak debug options.Maxime Dénès
2017-05-25Merge PR#637: Short cleaning of the interpretation path for constr_with_bindingsMaxime Dénès
2017-05-25Merge PR#608: Allow Ltac2 as a pluginMaxime Dénès
2017-05-25Merge PR#416: Fix the way setoid_rewrite handles bindings.Maxime Dénès
2017-05-25Merge PR#481: [option] Remove support for non-synchronous options.Maxime Dénès
2017-05-25Merge PR#406: coq makefile2Maxime Dénès
2017-05-25Merge PR#402: Uniform attribute handling in interfacesMaxime Dénès
2017-05-25[location] [travis] Add overlays for located_switchEmilio Jesus Gallego Arias
2017-05-24[location] Fix warnings.Emilio Jesus Gallego Arias
2017-05-24[location] Renaming "CAst.ast" to "CAst.t"Matej Košík
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-24ROmega: division-aware ReflOmegaCore, allowing trace without termsPierre Letouzey
The trace only mentions the constant k by which we want to divide the equation, not anymore the equation we obtain after the division. Shorter trace, and it won't take much more time to perform the few Z.div than checking as currently the equality of the initial equation and the final equation multiplied by k.
2017-05-24[option] Remove support for non-synchronous options.Emilio Jesus Gallego Arias
Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers.
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-07 21:09:40 +0000