aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-02-28Merge PR #9621: [ide] only use Coq_config for the URL of the manualPierre-Marie Pédrot
Ack-by: JasonGross Reviewed-by: ejgallego Ack-by: gares Reviewed-by: ppedrot
2019-02-28Print location for type error in pattern variableGaëtan Gilbert
See #9616
2019-02-28[sphinx] Add warn option to coqtop directive.Théo Zimmermann
By default Coq warnings are made fatal when building the manual. If you want to show a command resulting in a warning, use the warn option. Preexisting warnings are either fixed or marked as expected.
2019-02-28[Gitlab-CI] Creates a deploy-templateVincent Laporte
To be used when pushing an artifact to a github repository
2019-02-28Merge PR #9578: Document primitive integersThéo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-02-28Merge PR #9649: [dune] Simple rule to generate Stdlib's documentation.Théo Zimmermann
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: rgrinberg
2019-02-27[ide] only use Coq_config for the URL of the manualEnrico Tassi
2019-02-27Merge PR #9622: Fix makefile deps for coqidePierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2019-02-27[make] coqide target needs STM workersEnrico Tassi
2019-02-27[ide] coqtop -> coqidetop in user messagesEnrico Tassi
2019-02-26Initialize styles so textual markers are used when color is not enabledJim Fehrle
2019-02-26[dune] Simple rule to generate Stdlib's documentation.Emilio Jesus Gallego Arias
Ideally this will be handled by Dune's native library support, but this could be useful for the likes of #9648. I am not sure what should be done w.r.t. style files.
2019-02-26Merge PR #9612: Fix #9526: Registering inductives for primitive integers ↵Vincent Laporte
doesn't check enough Ack-by: SkySkimmer Reviewed-by: vbgl
2019-02-26Fix deprecation warningEnrico Tassi
2019-02-26[default.nix] Enable parallel buildVincent Laporte
2019-02-26Fix #9526: Registering inductives for primitive integers doesn't check enoughMaxime Dénès
2019-02-26Merge PR #9648: [Gitlab-CI] Deploy api documentation to GH-PagesEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego Ack-by: vbgl
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-25 21:09:18 +0000