aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Unified terminology in configure.ml/coq_config.ml: arch_win32 -> arch_is_win32.Gravatar Hugo Herbelin2017-05-29
|
* Mini-renaming in configure.ml to avoid switching back and forth fromGravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | | | | | | | | | | "libdir" to "COQLIBINSTALL" then "libdir", then "coqlib". For the record, here is how installation options are named at the current time in the different places they are used (if any): Name in Name in Name in Name of option Name in Name of option config/Makefile coqtop -config config/coq_config.ml in configure lib/envars.ml for coqtop/coqdep -------------------------------------------------------------------------------------------------------- COQLIBINSTALL COQLIB coqlib -libdir coqlib -coqlib DOCDIR DOCDIR docdir -docdir docdir CONFIGDIR configdir -configdir DATADIR datadir -datadir BINDIR -bindir MANDIR -mandir EMACSLIB -emacslib COQDOCDIR -coqdocdir Note: in envars.ml, docdir and coqlib are recomputed
* Dead code (xdg_config_dirs).Gravatar Hugo Herbelin2017-05-29
|
* Merge PR#675: [coqlib] Deprecate redundant Coqlib functions.Gravatar Maxime Dénès2017-05-28
|\
* \ Merge PR#683: coq_makefile: build .cma for each .mlpackGravatar Maxime Dénès2017-05-28
|\ \
* \ \ Merge PR#684: Trunk+fix coq makefile test suite on nixosGravatar Maxime Dénès2017-05-28
|\ \ \
* \ \ \ Merge PR#681: Fix votour for safe strings & warningsGravatar Maxime Dénès2017-05-28
|\ \ \ \
* \ \ \ \ Merge PR#680: add Show test with -emacs flag for trunkGravatar Maxime Dénès2017-05-28
|\ \ \ \ \
* \ \ \ \ \ Merge PR#676: Primitive Ltac definitions for first and solveGravatar Maxime Dénès2017-05-28
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR#658: [coqdoc] Add keywords in bug 2884.Gravatar Maxime Dénès2017-05-28
|\ \ \ \ \ \ \
| | | | | | | * [coqlib] Deprecate redundant Coqlib functions.Gravatar Emilio Jesus Gallego Arias2017-05-27
| |_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
| | | | | | * coq_makefile: build .cma for each .mlpackGravatar Enrico Tassi2017-05-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
| | * | | | | Documenting the existence of first and solve as Ltac definitions.Gravatar Pierre-Marie Pédrot2017-05-27
| | | | | | |
| | * | | | | Exporting a few primitive tacticals as named Ltac definitions.Gravatar Pierre-Marie Pédrot2017-05-27
| |/ / / / / |/| | | | |
* | | | | | Merge PR#686: [travis] temporary UniMath overlayGravatar Maxime Dénès2017-05-27
|\ \ \ \ \ \
| * | | | | | [travis] temporary UniMath overlayGravatar Maxime Dénès2017-05-27
|/ / / / / / | | | | | | | | | | | | | | | | | | We are waiting for an upstream merge of a fix related to coq_makefile2.
| | | | * | Add execution permission to test-suite file.Gravatar Théo Zimmermann2017-05-27
| | | | | |
| | | | * | Use specific shell for more robustness.Gravatar Théo Zimmermann2017-05-27
| | | | | |
| | | | * | Fix test-suite/coq-makefile on NixOS.Gravatar Théo Zimmermann2017-05-27
| |_|_|/ / |/| | | |
| | | * | Merge pull request #7 from SkySkimmer/checker+fix_votourGravatar Emilio Jesús Gallego Arias2017-05-26
| | | |\ \ | | | | | | | | | | | | [checker] [votour] resolve warning 52 fragile constant pattern
| | | | * | [checker] [votour] resolve warning 52 fragile constant patternGravatar Gaëtan Gilbert2017-05-26
| | | |/ / | | | | | | | | | | | | | | | Also stop using failwith for flow control in tuple_of_string.
* | | | | Merge PR#666: romega revisited : no more normalization trace, cleaned-up ↵Gravatar Maxime Dénès2017-05-26
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | resolution trace
* \ \ \ \ \ Merge PR#655: Extra functions exported in EConstrGravatar Maxime Dénès2017-05-26
|\ \ \ \ \ \ | |_|_|_|_|/ |/| | | | |
| | | | | * [checker] Add bin/votour to the coqocaml target.Gravatar Emilio Jesus Gallego Arias2017-05-26
| | | | | |
| | | | | * [votour] Fix/disable warnings.Gravatar Emilio Jesus Gallego Arias2017-05-26
| | | | | |
| | | | | * [votour] Fix build with -safe-string (bug 5553)Gravatar Emilio Jesus Gallego Arias2017-05-26
| |_|_|_|/ |/| | | |
| | | | * add Show test with -emacs flagGravatar Paul Steckler2017-05-25
| |_|_|/ |/| | |
* | | | Merge PR#645: [stm] Tweak debug options.Gravatar Maxime Dénès2017-05-25
|\ \ \ \
* \ \ \ \ Merge PR#637: Short cleaning of the interpretation path for constr_with_bindingsGravatar Maxime Dénès2017-05-25
|\ \ \ \ \
* \ \ \ \ \ Merge PR#608: Allow Ltac2 as a pluginGravatar Maxime Dénès2017-05-25
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR#406: coq makefile2Gravatar Maxime Dénès2017-05-25
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR#402: Uniform attribute handling in interfacesGravatar Maxime Dénès2017-05-25
|\ \ \ \ \ \ \ \ \
| * | | | | | | | | [location] [travis] Add overlays for located_switchGravatar Emilio Jesus Gallego Arias2017-05-25
| | | | | | | | | |
| * | | | | | | | | [location] Fix warnings.Gravatar Emilio Jesus Gallego Arias2017-05-24
| | | | | | | | | |
| * | | | | | | | | [location] Renaming "CAst.ast" to "CAst.t"Gravatar Matej Košík2017-05-24
| | | | | | | | | |
| * | | | | | | | | Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
| |\ \ \ \ \ \ \ \ \ | |/ / / / / / / / / |/| | | | | | | | |
| | | | | | | | * | ROmega: division-aware ReflOmegaCore, allowing trace without termsGravatar Pierre Letouzey2017-05-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | * | | | | | | [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * | | | | | | | coq_makefile: use -include rather than includeGravatar Enrico Tassi2017-05-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This fixes bedrock and eliminates warnings. Thanks Jason Gross for debugging this!
* | | | | | | | | | Merge PR#642: Small cleanup on `close_proof` type.Gravatar Maxime Dénès2017-05-24
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR#650: Fixing an extra bug with pattern_of_constrGravatar Maxime Dénès2017-05-24
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR#671: unification.mli: Fix a spelling typo in a commentGravatar Maxime Dénès2017-05-24
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|/ / / / / / / |/| | | | | | | | | | |
| * | | | | | | | | | | unification.mli: Fix a spelling typo in a commentGravatar Jason Gross2017-05-23
|/ / / / / / / / / / /
| | | | * | | | | | | add the only targetGravatar Enrico Tassi2017-05-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This makes the following work correctly: make only TGTS="foo bar" -j2 note that make foo bar -j2 is not doing what you think
| | | | * | | | | | | travis: coq_makefile needs the tipa packageGravatar Enrico Tassi2017-05-23
| | | | | | | | | | |
| | | | * | | | | | | overlay for UniMathGravatar Enrico Tassi2017-05-23
| | | | | | | | | | |
| | | | * | | | | | | coq_makefile: avoid spurious ./ in generated .conf fileGravatar Enrico Tassi2017-05-23
| | | | | | | | | | |
| | | | * | | | | | | Restore 8.5, 8.6 compatibility of STDTIME, TIMECMDGravatar Jason Gross2017-05-23
| | | | | | | | | | |
| | | | * | | | | | | coq_makefile: don't quote extra arguments (-arg)Gravatar Enrico Tassi2017-05-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Restores compatibility with 8.6
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 12:05:30 +0000