aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Collapse)AuthorAge
* Merge PR #898: [pp] Fix bugs 5651 [incorrect thunk in pretty printer]Gravatar Maxime Dénès2017-07-20
|\
* \ Merge PR #869: Enforce alternating separators in typeclass debug outputGravatar Maxime Dénès2017-07-20
|\ \
| | * [pp] Fix bugs 5651 [incorrect thunk in pretty printer]Gravatar Emilio Jesus Gallego Arias2017-07-19
| |/ |/| | | | | Fix bug introduced by a Haskell programmer.
* | Merge PR #862: Adding support for bindings tags to explicit prefix/suffix ↵Gravatar Maxime Dénès2017-07-17
|\ \ | | | | | | | | | rather than colors
| | * format pairs of items for pr_depth to get alternating separatorsGravatar Paul Steckler2017-07-12
| | | | | | | | | | | | | | | eval thunks once in prlist_sep_lastsep, make code clearer add typeclass debug output test
| * | Adding support for bindings tags to explicit prefix/suffix rather than colors.Gravatar Hugo Herbelin2017-07-08
| |/ | | | | | | | | | | | | | | This is usable for no-color terminal. For instance, a typical application in mind is the Coq-generate names marker which can be rendered with a color if the interface supports it and a prefix "~" if the interface does not support colors.
* / use Int.equal instead of polymorphic =Gravatar Paul Steckler2017-07-05
|/
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| |
| * Fix bug 5392: Warnings defined in plugins are considered unknownGravatar Maxime Dénès2017-06-23
| | | | | | | | | | | | The status of a warning can now be set before the warning is declared (typically by a plugin). However, I had to remove the "unknown warning" warning.
* | Merge PR#613: Cumulativity for inductive typesGravatar Maxime Dénès2017-06-19
|\ \
* | | Fix typo in comment.Gravatar Maxime Dénès2017-06-19
| | |
| * | Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
|/ /
* | Merge PR#375: DeprecationGravatar Maxime Dénès2017-06-15
|\ \
* \ \ Merge PR#739: completing a sentence in a commentGravatar Maxime Dénès2017-06-14
|\ \ \
| | * | Remove support for Coq 8.4.Gravatar Guillaume Melquiond2017-06-14
| | | |
| | * | Remove support for Coq 8.3.Gravatar Guillaume Melquiond2017-06-14
| | | |
| | * | Remove support for Coq 8.2.Gravatar Guillaume Melquiond2017-06-14
| | | |
| | * | Add a version to be used when parsing compatibility notations mentioning old ↵Gravatar Guillaume Melquiond2017-06-14
| |/ / |/| | | | | | | | versions.
* | | Add support for "-bypass-API" argument of "coq_makefile"Gravatar Matej Košík2017-06-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Plugin-writers can now use: -bypass-API parameter with "coq_makefile". The effect of that is that instead of -I API the plugin will be compiled with: -I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac
| * | completing a sentence in a commentGravatar Matej Košík2017-06-07
| | |
* | | Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
|/ /
* | Merge PR#728: A few typos.Gravatar Maxime Dénès2017-06-06
|\ \
| * | A few typos.Gravatar Hugo Herbelin2017-06-04
| | |
* | | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ```
* | [emacs] [toplevel] Make emacs flag local to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-06-01
| | | | | | | | | | We remove the emacs-specific printing code from the core of Coq, now `-emacs` is a printing flag controlled by the toplevel.
| * Bump year in headers.Gravatar Maxime Dénès2017-06-01
| |
* | Merge PR#356: Making management of installation directories more structured, ↵Gravatar Maxime Dénès2017-05-30
|\ \ | | | | | | | | | more uniform
* \ \ Merge PR#692: Fail on deprecated warning even for Ocaml > 4.02.3Gravatar Maxime Dénès2017-05-30
|\ \ \
| | * | Relying on computation done in Envars to discover the installation directories.Gravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | | | | | This allows to share the test for possible relocalisation done in envars.ml.
| | * | Generalizing to docdir and datadir the test for a relocated installation.Gravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Also standardizing the choice of the default datadir (I don't see why we should add by default both /usr/local/share/coq and /usr/share/coq when we know that the installation is in only one of them). Open question: test for possible relocation of the installed coq should be done on raw dirname of the executable or on the standardization of this name wrt symbolic links?
| | * | Exporting the suffixes needed to build coqlib, docdir, etc.Gravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows to centralize in the configuration file the description of the 3 possible installation layouts (dispatched over directories shared by multiple application as in unix, self-contained style like in windows, local non-installation as with option -local). Also supporting relocalisation when -prefix or -libdir and co is given.
| | * | Using Coq_config.local rather than None to tell that Coq_config.coqlib is local.Gravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | | | | | | | | | This goes towards an approach where a local layout can be seen as an installed layout.
| | * | Configuration: always giving a value to configdir and datadir.Gravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | They were not used for looking for coqide files in the situation when the effective installation path happens to be exactly the installation path proposed by default, while relevant files were however (possibly) installed in these directories.
| | * | Dead code (xdg_config_dirs).Gravatar Hugo Herbelin2017-05-29
| | | |
| * | | Fail on deprecated warning even for Ocaml > 4.02.3Gravatar Gaëtan Gilbert2017-05-28
| |/ / | | | | | | | | | | | | | | | | | | | | | Deprecations which can't be fixed in 4.02.3 are locally wrapped with [@@@ocaml.warning "-3"]. The only ones encountered are - capitalize to capitalize_ascii and variants. Changing to ascii would break coqdoc -latin1 and maybe other things though. - external "noalloc" to external [@@noalloc]
* / / [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
|/ / | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | 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
|\ \ \
* \ \ \ Merge PR#645: [stm] Tweak debug options.Gravatar Maxime Dénès2017-05-25
|\ \ \ \
* \ \ \ \ Merge PR#406: coq makefile2Gravatar Maxime Dénès2017-05-25
|\ \ \ \ \
* | | | | | [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
|\ \ \ \ \ \
| | * | | | | coq_makefile: avoid spurious ./ in generated .conf fileGravatar Enrico Tassi2017-05-23
| | | | | | |
| | * | | | | enters coq_makefile2Gravatar Enrico Tassi2017-05-23
| | | | | | |
| | * | | | | ocamlfind: coqtop -config prints ocamlfind as found by ./configureGravatar Enrico Tassi2017-05-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Used to guess again the ocamlfind location at Coq's execution time. An option to override the value (inferred at ./configure time) is available. So, what is the point of guessing it? Either it stays there, or the user is doing a hack, and has a flag to do it.
| | * | | | | print_config: print COQ_SRC_SUBDIRSGravatar Enrico Tassi2017-05-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This way a makefile can just iterate on this list, intead of having a bunch of -I hardcoded in there by coq_makefile
| | * | | | | Put the list of Coq sources subdirectories in one placeGravatar Enrico Tassi2017-05-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | and avoid duplication
| | * | | | | Usage.print_config moved to EnvarsGravatar Enrico Tassi2017-05-23
| | | | | | |
| | * | | | | CoqProject_file: document in API deprecated featuresGravatar Enrico Tassi2017-05-23
| | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 12:04:09 +0000