aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-02-26Merge PR #9653: Fix gitattributes for Makefile.duneEmilio Jesus Gallego Arias
2019-02-26Fix gitattributes for Makefile.duneGaëtan Gilbert
Since it matches *.dune and Makefile* the later needs to come second in the gitattributes file.
2019-02-26Merge PR #9567: [vernac] Unify declaration hooks.Maxime Dénès
Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: mattam82 Reviewed-by: maximedenes
2019-02-25add testcase for primitive projectionEnrico Tassi
2019-02-25Fix #9631: Instance: anomaly grounding non evar-free termGaëtan Gilbert
2019-02-25[kernel] termination checking backtracks on stuck primitive projectionEnrico Tassi
2019-02-25add testcase for fixEnrico Tassi
2019-02-25[kernel] termination checking backtracks on stuck fixEnrico Tassi
2019-02-25add test case for "match"Enrico Tassi
2019-02-25[Manual] Refactor documentation of internal registration commandsVincent Laporte
2019-02-25[Manual] Document primitive integersVincent Laporte
2019-02-25[Manual] Document the “Primitive” commandVincent Laporte
2019-02-25[Manual] Document “Register Inline”Vincent Laporte
2019-02-25[Manual] Document “Register” to kernel namespaceVincent Laporte
2019-02-25Merge PR #9620: Stdlib HTML documentation: fix a few absolute URLsThéo Zimmermann
Reviewed-by: Zimmi48
2019-02-25Merge PR #9511: Enable whitespace checking for some forgotten files.Théo Zimmermann
Reviewed-by: Zimmi48
2019-02-25[Gitlab-CI] Deploy api documentation to GH-PagesVincent Laporte
2019-02-23[vernac] Unify declaration hooks.Emilio Jesus Gallego Arias
Supersedes #8718.
2019-02-22update CHANGESEnrico Tassi
2019-02-22overlay for EquationsEnrico Tassi
2019-02-22[kernel] termination checking backtracks on stuck caseEnrico Tassi
The strategy is to backtrack when a constant is in head position: we first try to see if the arguments are guarded, if not we unfold. Since `Case` is represented as a head (rather than as a context as the reduction machine does) we did not backtrack there and reduce (including delta) the scrutinized in order to fire the iota redex. This commit adds a choice point in that specific case, and reduces eagerly (not step by step) the scrutinized in case of failure.
2019-02-22Merge PR #9364: Apply implicit binders to Hypothesis inside sections.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-02-22Merge PR #9576: [library] Remove `-boot` option.Enrico Tassi
Reviewed-by: SkySkimmer Ack-by: ejgallego Reviewed-by: gares
2019-02-22Apply implicit binders to Hypothesis inside sections.Jasper Hugunin
2019-02-22Merge PR #9561: [dev] Add include versions for Dune builds.Théo Zimmermann
Reviewed-by: Zimmi48
2019-02-22Merge PR #9314: Enrich implicits for instancesGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-02-22Merge PR #9539: [coqdoc] Add the From keywordGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-02-22Implement hmap.updateGaëtan Gilbert
2019-02-22[library] Remove `-boot` option.Emilio Jesus Gallego Arias
The `-boot` option was used to: - suppress loading of the rc_file - allow to save modules with prefix `Coq` There is no good reason disable saving of modules with `Coq` prefix by default, thus we remove this option. Fixes: #9575
2019-02-22[lib] Add `Map.update` from OCaml 4.06Emilio Jesus Gallego Arias
It will take more than a year to bump the OCaml version, this is in response of a request by @Skyskimmer. We also update our internal repr to make it closer to the one in modern OCaml.
2019-02-22Merge PR #9614: Fix #9613 use -coqlib when invoking coqchkEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-02-21Merge PR #9588: [azure] [ci] Build on Windows using Dune.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-02-21Stdlib HTML documentation: fix a few absolute URLsVincent Laporte
2019-02-21Merge PR #9577: [Namegen] Use Global.exists_objlabel in `next_global_ident_away`Pierre-Marie Pédrot
Reviewed-by: maximedenes Reviewed-by: ppedrot
2019-02-21Merge PR #9618: [dev/tools/create_overlays] remove trailing whitespaceEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-02-21remove meta trailing whitespaceEnrico Tassi
2019-02-21Fix #9613 use -coqlib when invoking coqchkGaëtan Gilbert
In passing add -coqlib to coqchk's usage message.
2019-02-21Merge PR #9388: merge-pr.sh: fix #9387: quick_conf doesn't work in emacs ↵Emilio Jesus Gallego Arias
shell buffer Reviewed-by: ejgallego
2019-02-20Merge PR #9529: Change Primitive message: "is registered" -> "is declared".Vincent Laporte
Reviewed-by: vbgl
2019-02-20Enable whitespace checking for some forgotten files.Gaëtan Gilbert
+ remove checker/.depend forgotten file
2019-02-20Merge PR #9457: Correct W-Ind in Cic description of the reference manual.Théo Zimmermann
Reviewed-by: SkySkimmer
2019-02-20[paths] Try to be more portable on Win32Emilio Jesus Gallego Arias
Absolute paths follow different separator rules so "c:\foo/bar" may not work on `mingw`. We try to improve this situation using OCaml's `Filename.dir_sep/concat`
2019-02-20[azure] [ci] Build on Windows using Dune.Emilio Jesus Gallego Arias
We may want to keep the make-based and Dune job, however the make-based setup is tested by the INRIA workers so it may not be needed. In order for some test to run well, we always run in Dune with an absolute path. The easiest way to get a portable absolute path is to use OCaml itself so we introduce a small executable to do that. While we are at it, we do some cleanup of the test-suite `dune` file, in particular we remove useless comments, set `--no-buffer` so results can be seen in real time, and recognize the `NJOBS` variable as we have moved to a Dune version that supports env vars.
2019-02-20Merge PR #9560: [coqlib] Remove `-boot` option for setting the coqlibEnrico Tassi
Reviewed-by: SkySkimmer Ack-by: ejgallego Reviewed-by: gares
2019-02-20Merge pull request coq/ltac2#108 from ejgallego/fix_warnPierre-Marie Pédrot
[coq] Fix OCaml warnings.
2019-02-20[coq] Fix OCaml warnings.Emilio Jesus Gallego Arias
In anticipation to https://github.com/coq/coq/pull/9605 , we fix all OCaml warnings. Fixes coq/ltac2#107
2019-02-19Merge PR #9501: Sphinx: fail when a command fails + other stuffClément Pit-Claudel
Ack-by: SkySkimmer Ack-by: gares Reviewed-by: Zimmi48 Reviewed-by: cpitclaudel Reviewed-by: ejgallego
2019-02-19Merge PR #9297: Two fixes in printing notations with patternsEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Ack-by: herbelin Reviewed-by: mattam82
2019-02-19Merge PR #9604: Gramlib: Fixes #9358 (ensuring that requested locations are ↵Emilio Jesus Gallego Arias
effectively computed at lexing time) Reviewed-by: ejgallego
2019-02-19Merge PR #9603: Make inductive cumulativity flag local to vernacentriesEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-22 18:58:49 +0000