aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-11-28Moving non-recursive function sort_family_of out of the retype block of ↵Hugo Herbelin
recursive functions.
2017-11-28Adding an interface file for checker/check.ml.Pierre-Marie Pédrot
2017-11-28more complete not-fully-applied error messages, #6145Paul Steckler
2017-11-28Add PR backport script.Théo Zimmermann
2017-11-28[toplevel] Properly redirect stdout on `Redirect` vernac.Emilio Jesus Gallego Arias
Fixes #6130, it was a silly omission from a previous output refactoring. We redirect all channels as this was the implied semantics of the old command.
2017-11-28[ci] [vst] Shorten compilation time to avoid Travis timeouts.Emilio Jesus Gallego Arias
We remove the progs target [examples] to save time, we still build the full library thou. I guess we can't do better for now unless we get some Travis subscription.
2017-11-28Use safe demarshalling in the checker.Pierre-Marie Pédrot
Instead of relying on the OCaml demarshaller, which is not resilient against ill-formed data, we reuse the safe demarshaller from votour. This ensures that garbage files do not trigger memory violations.
2017-11-28Use large arrays in the checker demarshaller.Pierre-Marie Pédrot
This allows to work around the size limitation of vanilla OCaml arrays on 32-bit platforms, which is rather easy to hit.
2017-11-28CI: use -byte-only in [warnings] jobs.Gaëtan Gilbert
This avoids mixing native and byte compilation as the debug printers are always byte compiled and the tools have no .byte rule, only the OCAMLBEST rule.
2017-11-28Fix native compute for byte compiled Coq.Gaëtan Gilbert
2017-11-28Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gaëtan Gilbert
2017-11-28Make the micromega extraction check a regular output test.Gaëtan Gilbert
This allows us to enforce that it works without breaking the build when it doesn't.
2017-11-28Travis: do not build stdlib in [warnings] jobs.Gaëtan Gilbert
2017-11-28Add alienclean target to remove compilation products with no source.Gaëtan Gilbert
2017-11-28Merge PR #6259: Add PR merge script.Maxime Dénès
2017-11-28Add PR merge script.Maxime Dénès
2017-11-28Merge PR #1033: Universe binder improvementsMaxime Dénès
2017-11-28Merge PR #6235: Fixing failing mkdir in test-suite for coq-makefile.Maxime Dénès
2017-11-28Merge PR #6248: [api] Remove aliases of `Evar.t`Maxime Dénès
2017-11-28Merge PR #6246: Ref. Man.: Updating the current official writing of OCaml; ↵Maxime Dénès
updating Camlp4->Camlp5.
2017-11-27allow :: and , as infix opsPaul Steckler
2017-11-27[vernac] Adjust `interp` to pass polymorphic in the attributes.Emilio Jesus Gallego Arias
2017-11-27[vernac] Add polymorphic to the type of vernac interpration options.Emilio Jesus Gallego Arias
2017-11-27[vernac] Start to uniformize type of vernac interpretation.Emilio Jesus Gallego Arias
In particular, we put all the context in the atts structure, and generalize the type of the parameters of a vernac. I hope this helps people working on "attributes", my motivation is indeed having a more robust interpretation.
2017-11-27Selecting which notation to print based on current stack of scope.Hugo Herbelin
See discussion on coq-club starting on 23 August 2016. An open question: what priority to give to "abbreviations"?
2017-11-27Pre-isolating a notation test to avoid interferences.Hugo Herbelin
2017-11-27Adding overlay for ltac2.Hugo Herbelin
2017-11-27Merge PR #6237: coq_makefile tests: build in easily removed temporary ↵Maxime Dénès
subdirectory.
2017-11-27Merge PR #6242: Use Evarutil.has_undefined_evars for tactic has_evar.Maxime Dénès
2017-11-27Merge PR #6236: Fix coq-makefile ocamldoc call when configured with -annotate.Maxime Dénès
2017-11-27Merge PR #6207: [stm] Allow delayed constant in interactive mode.Maxime Dénès
2017-11-27Merge PR #6238: Fix deprecated syntax warning from vernacextend.mlp.Maxime Dénès
2017-11-27Merge PR #6241: [lib] Generalize Control.timeout type.Maxime Dénès
2017-11-27Merge PR #6228: Make byte on gitlab.Maxime Dénès
2017-11-27Merge PR #6226: Enhance votourMaxime Dénès
2017-11-27Merge PR #6149: Update TimeFileMaker.py to correctly sort timing diffsMaxime Dénès
2017-11-27Merge PR #6041: Protecting the printing of filenames with spaceMaxime Dénès
2017-11-27Merge PR #6227: Linter: do not lint untracked files.Maxime Dénès
2017-11-27A cosmetic standardization: adding a space in g_constr.ml4.Hugo Herbelin
2017-11-27Releasing level "11" of "pattern".Hugo Herbelin
Was introduced in 0917ce7c to fix #4272, but it seems that we can fix it by just merging levels 10 and 11. This prevents the worry of fixing the associativity of level 11 to left in 0917ce7c.
2017-11-27Fixing associativity registered for level 10.Hugo Herbelin
Apparently a long-standing bug, coupled with a pattern/constr associativity inconsistency introduced while fixing another pattern/constr level inconsistency (bug #4272, 0917ce7c).
2017-11-26[api] Remove aliases of `Evar.t`Emilio Jesus Gallego Arias
There don't really bring anything, we also correct some minor nits with the printing function.
2017-11-25Overlay for stronger restrict_universe_context.Gaëtan Gilbert
2017-11-25Restrict universe context when declaring constants in obligations.Gaëtan Gilbert
2017-11-25Updating the current official writing of OCaml, updating Camlp4->Camlp5.Hugo Herbelin
2017-11-25Fix #5347: unify declaration of axioms with and without bound univs.Gaëtan Gilbert
Note that this makes the following syntax valid: Axiom foo@{i} bar : Type@{i}. (ie putting a universe declaration on the first axiom in the list, the declaration then holds for the whole list).
2017-11-25Fix interpretation of global universes in univdecl constraints.Gaëtan Gilbert
Also nicer error when the constraints are impossible.
2017-11-25Forbid repeated names in universe binders.Gaëtan Gilbert
2017-11-25Universe binders survive sections, modules and compilation.Gaëtan Gilbert
2017-11-25Allow local universe renaming in Print.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-01 04:50:54 +0000