aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-03-16Add test-suite to Paramcoq CIPierre Roux
2019-03-15Merge PR #9783: [ci] [gitlab] Replace YAML grafting by `extends: ` declaration.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-03-15[ci] [gitlab] Replace YAML grafting by `extends: ` declaration.Emilio Jesus Gallego Arias
This should in general be more robust as we don't need to remember to graft subsections.
2019-03-15Merge PR #9694: remove unused import of osEmilio Jesus Gallego Arias
Reviewed-by: JasonGross
2019-03-15Merge PR #8817: SProp: the definitionally proof irrelevant universePierre-Marie Pédrot
Ack-by: JasonGross Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: mattam82
2019-03-15Merge PR #9425: BinInt: 3 lemmas about testbit, mod _ 2^, onesVincent Laporte
Reviewed-by: vbgl
2019-03-14Merge PR #9771: Exposes Coq_micromega.dump_proof_term to allow a use ↵Vincent Laporte
independent from tactics Reviewed-by: vbgl
2019-03-14Fix various dummy Relevant in ssrGaëtan Gilbert
Unknown impact so no tests.
2019-03-14Overlays for SPropGaëtan Gilbert
2019-03-14Documentation for SPropGaëtan Gilbert
2019-03-14Add StrictProp.v with basic SProp related definitionsGaëtan Gilbert
2019-03-14Put [@inline] on CClosure.Mark functionsGaëtan Gilbert
2019-03-14Switch order eqappr/check relevance in conversion.Gaëtan Gilbert
This takes advantage of the mutability of the fconstr relevance mark.
2019-03-14mutable relevance marks in fconstrGaëtan Gilbert
2019-03-14Test for SkySkimmer/coq#13Gaëtan Gilbert
(NB: this needs relevance mark fixing)
2019-03-14Repair relevance marks in-kernel.Gaëtan Gilbert
Prevent errors when under annotating binders.
2019-03-14Enable proof irrelevance for SProp.Gaëtan Gilbert
2019-03-14Inductives in SProp, forbid primitive records with only sprop fieldsGaëtan Gilbert
For nonsquashed: Either - 0 constructors - primitive record
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
Kernel should be mostly correct, higher levels do random stuff at times.
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
Note currently it's impossible to define inductives in SProp because indtypes.ml and the pretyper aren't fully plugged.
2019-03-14Make Sorts.t privateGaëtan Gilbert
2019-03-14Fix Require in output test for reals syntaxGaëtan Gilbert
2019-03-14BinInt: 3 lemmas about testbit, mod _ 2^, onesAndres Erbsen
2019-03-14Merge PR #9691: [dune] [ide] Don't install the internal CoqIDE UI library.Théo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2019-03-14Merge PR #9700: [dune] [checker] Don't install internal checker library.Théo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2019-03-14Exposes Coq_micromega.dump_proof_term to allow a use independent from tacticsChantal Keller
2019-03-13Merge PR #9736: Don't coqchk the test suite prerequisitesEnrico Tassi
Reviewed-by: gares
2019-03-13Merge PR #9757: [refman] Add 'warn' option to coqtop directive.Emilio Jesus Gallego Arias
Reviewed-by: cpitclaudel
2019-03-13Merge PR #9723: Fix undefined gramlib_MLLIB_DEPENDENCIES in make installEnrico Tassi
Reviewed-by: gares
2019-03-13Merge PR #9739: [dune] [configure] Fix `gramlib` path for hardcoded includes.Enrico Tassi
Reviewed-by: gares
2019-03-13Merge PR #9748: [dune] Add shim for coqtop.byteThéo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: gares
2019-03-13[refman] Fix Sphinx-translation regression in Arguments command.Théo Zimmermann
2019-03-13[refman] Remove warning silencing by fixing the underlying issue.Théo Zimmermann
2019-03-13[refman] Fix other newly emitted warnings.Théo Zimmermann
2019-03-13Merge PR #9627: Small retroknowledge/primitive cleanupVincent Laporte
Ack-by: SkySkimmer Reviewed-by: ppedrot Reviewed-by: vbgl
2019-03-12[refman] Add 'warn' option to coqtop directive.Théo Zimmermann
Fix semantic conflict between #9389 and #9654.
2019-03-12Merge PR #9632: Fix #9631: Instance: anomaly grounding non evar-free termEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego Ack-by: ppedrot
2019-03-12Merge PR #9596: Fix #9595: missing non-primitive-record warning with 0 field ↵Emilio Jesus Gallego Arias
record Reviewed-by: ejgallego
2019-03-12Merge PR #9389: Implement a method for manual declaration of implicits.Emilio Jesus Gallego Arias
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: jashug
2019-03-12Merge PR #7819: Ho matching occ selEnrico Tassi
Ack-by: gares Ack-by: herbelin Ack-by: mattam82 Ack-by: ppedrot
2019-03-12[dune] Add shim for coqtop.byteEmilio Jesus Gallego Arias
We add a shim for running the byte version of coqtop. This fixes the Coq part of #9727 , the Dune part is still open at https://github.com/ocaml/dune/issues/108 but this PR includes a workaround. Unfortunately we have to introduce a small inefficiency in the build process as we build both byte and native versions of plugins for this work reliable. As this is a choice done during bootstrap it won't be easy to fix until we have our own `dune coqtop` command and we can control the rules depending on the final target. This should affect the `check` target so still fast builds should be possible, but if this is a problem we could add a `byteboot` target to help.
2019-03-12Merge PR #9738: [ci] [docker] Upgrade odoc to 1.4.0Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-03-11[dune] [configure] Fix `gramlib` path for hardcoded includes.Emilio Jesus Gallego Arias
The regular make build uses a non-standard header path for their files [as a way to workaround the ugliness of the non-hygienic build] This breaks in Dune as it uses the regular object file pack, so `coq_makefile` won't find it. We cherry pick a change from #8729 which fixes the updated version of bug #9735 , even tho `coq_makefile` should stop relying on hardcoded paths and use findlib instead. Closes #9735
2019-03-11[ci] [docker] Upgrade odoc to 1.4.0Emilio Jesus Gallego Arias
This is routine as for API doc writers to be able to access the newer features.
2019-03-11Don't coqchk the test suite prerequisitesGaëtan Gilbert
This causes the makefile to break due to dependencies when it fails, and it's not worth adding a whole mess of code to catch the failure for these files.
2019-03-11Fix undefined gramlib_MLLIB_DEPENDENCIES in make installGaëtan Gilbert
2019-03-11Nicer error for bad primitive types (through type_errors etc)Gaëtan Gilbert
2019-03-11Remove unused Retroknowledge.Register_inlineGaëtan Gilbert
This operation is done directly in Safe_typing.register_inline and has nothing to do with retroknowledge afaict.
2019-03-11Merge PR #9698: Remove last random failuresGaëtan Gilbert
Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: ejgallego
2019-03-11Merge PR #9675: Dune: remove -short-paths flag.Emilio Jesus Gallego Arias
Ack-by: ejgallego Reviewed-by: gares
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 21:56:41 +0000