| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-28 | Merge PR#678: [coqlib] Move `Coqlib` to `library/`. | Maxime Dénès | |
| 2017-05-28 | Merge PR#689: Changes to make coq-makefile not failing on MacOS X. | Maxime Dénès | |
| 2017-05-28 | Merge PR#675: [coqlib] Deprecate redundant Coqlib functions. | Maxime Dénès | |
| 2017-05-28 | Merge PR#683: coq_makefile: build .cma for each .mlpack | Maxime Dénès | |
| 2017-05-28 | Merge PR#684: Trunk+fix coq makefile test suite on nixos | Maxime Dénès | |
| 2017-05-28 | Merge PR#681: Fix votour for safe strings & warnings | Maxime Dénès | |
| 2017-05-28 | Merge PR#680: add Show test with -emacs flag for trunk | Maxime Dénès | |
| 2017-05-28 | Merge PR#676: Primitive Ltac definitions for first and solve | Maxime Dénès | |
| 2017-05-28 | Merge PR#658: [coqdoc] Add keywords in bug 2884. | Maxime Dénès | |
| 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-27 | coq_makefile: build .cma for each .mlpack | Enrico 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-27 | Documenting the existence of first and solve as Ltac definitions. | Pierre-Marie Pédrot | |
| 2017-05-27 | Exporting a few primitive tacticals as named Ltac definitions. | Pierre-Marie Pédrot | |
| 2017-05-27 | Merge PR#686: [travis] temporary UniMath overlay | Maxime Dénès | |
| 2017-05-27 | [travis] temporary UniMath overlay | Maxime Dénès | |
| We are waiting for an upstream merge of a fix related to coq_makefile2. | |||
| 2017-05-27 | Add execution permission to test-suite file. | Théo Zimmermann | |
| 2017-05-27 | Use specific shell for more robustness. | Théo Zimmermann | |
| 2017-05-27 | Fix test-suite/coq-makefile on NixOS. | Théo Zimmermann | |
| 2017-05-26 | Changes 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-26 | Merge pull request #7 from SkySkimmer/checker+fix_votour | Emilio Jesús Gallego Arias | |
| [checker] [votour] resolve warning 52 fragile constant pattern | |||
| 2017-05-26 | [checker] [votour] resolve warning 52 fragile constant pattern | Gaëtan Gilbert | |
| Also stop using failwith for flow control in tuple_of_string. | |||
| 2017-05-26 | Merge PR#666: romega revisited : no more normalization trace, cleaned-up ↵ | Maxime Dénès | |
| resolution trace | |||
| 2017-05-26 | Merge PR#655: Extra functions exported in EConstr | Maxime 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-25 | add Show test with -emacs flag | Paul Steckler | |
| 2017-05-25 | Merge PR#645: [stm] Tweak debug options. | Maxime Dénès | |
| 2017-05-25 | Merge PR#637: Short cleaning of the interpretation path for constr_with_bindings | Maxime Dénès | |
| 2017-05-25 | Merge PR#608: Allow Ltac2 as a plugin | Maxime Dénès | |
| 2017-05-25 | Merge PR#481: [option] Remove support for non-synchronous options. | Maxime Dénès | |
| 2017-05-25 | Merge PR#406: coq makefile2 | Maxime Dénès | |
| 2017-05-25 | Merge PR#402: Uniform attribute handling in interfaces | Maxime Dénès | |
| 2017-05-25 | [location] [travis] Add overlays for located_switch | Emilio 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-24 | Merge branch 'trunk' into located_switch | Emilio Jesus Gallego Arias | |
| 2017-05-24 | ROmega: division-aware ReflOmegaCore, allowing trace without terms | Pierre 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. | |||
| 2017-05-24 | coq_makefile: use -include rather than include | Enrico Tassi | |
| This fixes bedrock and eliminates warnings. Thanks Jason Gross for debugging this! | |||
| 2017-05-24 | Merge PR#642: Small cleanup on `close_proof` type. | Maxime Dénès | |
| 2017-05-24 | Merge PR#650: Fixing an extra bug with pattern_of_constr | Maxime Dénès | |
| 2017-05-24 | Merge PR#671: unification.mli: Fix a spelling typo in a comment | Maxime Dénès | |
| 2017-05-23 | unification.mli: Fix a spelling typo in a comment | Jason Gross | |
| 2017-05-23 | add the only target | Enrico Tassi | |
| This makes the following work correctly: make only TGTS="foo bar" -j2 note that make foo bar -j2 is not doing what you think | |||
| 2017-05-23 | travis: coq_makefile needs the tipa package | Enrico Tassi | |
| 2017-05-23 | overlay for UniMath | Enrico Tassi | |
| 2017-05-23 | coq_makefile: avoid spurious ./ in generated .conf file | Enrico Tassi | |
| 2017-05-23 | Restore 8.5, 8.6 compatibility of STDTIME, TIMECMD | Jason Gross | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |