aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-12-05Merge PR #6287: Add merlin to default.nixMaxime Dénès
2017-12-05Merge PR #6210: More complete not-fully-applied error messages, #6145Maxime Dénès
2017-12-04[configure] fix detection of `md5sum`Vincent Laporte
2017-12-04[default.nix] needs ncurses for the test-suiteVincent Laporte
2017-12-04[vernac] Couple of tweaks missing from previous PRs.Emilio Jesus Gallego Arias
2017-12-03Adding a test for #6304 (bug with fix in notations).Hugo Herbelin
2017-12-02Remove redundant Zcase from the checker.Pierre-Marie Pédrot
2017-12-02[kernel] Patch allowing to disable VM reduction.Emilio Jesus Gallego Arias
2017-12-01uninstall doc dir, not dev (which is not installed), #6007Paul Steckler
2017-12-01check for Num lib if OCaml >= 4.06, #6162Paul Steckler
2017-12-01clarify operation of sequences, #6095Paul Steckler
2017-12-01Fix #6297: handle constraints like (u+1 <= Set/Prop)Gaëtan Gilbert
2017-12-01proposed fix for issue #3213: extra variable m in Lt.S_predfredokun
2017-12-01Update CHANGESMatthieu Sozeau
2017-12-01Cleanup API for registering universe binders.Matthieu Sozeau
2017-12-01[refman] Expand a little on global universes.Matthieu Sozeau
2017-12-01Tests for global universe declarationsMatthieu Sozeau
2017-12-01Proper nametab handling of global universe namesMatthieu Sozeau
2017-12-01Documenting the -Q flag of coqchk.Pierre-Marie Pédrot
2017-12-01Merge PR #736: [ci] Test coqchk on the CompCert target.Maxime Dénès
2017-12-01Merge PR #6256: CI: better ocaml warning checksMaxime Dénès
2017-12-01Merge PR #6276: Coqchk accepts filenamesMaxime Dénès
2017-12-01Merge PR #6233: [proof] [api] Rename proof types in preparation for functiona...Maxime Dénès
2017-11-30Merge PR #1049: Remove obsolete localityMaxime Dénès
2017-11-30Merge PR #6244: [lib] [api] Introduce record for `object_prefix`Maxime Dénès
2017-11-30[ci] Test coqchk on the CompCert target.Théo Zimmermann
2017-11-30Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ...Maxime Dénès
2017-11-30Remove unused boolean from cl_context field of Typeclasses.typeclassGaëtan Gilbert
2017-11-30Add merlin in the dependencies of nix-shell only.Théo Zimmermann
2017-11-30Merge PR #6269: [ci] [vst] Shorten compilation time to avoid Travis timeouts.Maxime Dénès
2017-11-30Merge PR #6193: Fix (partial) #4878: option to stop autodeclaring axiom as in...Maxime Dénès
2017-11-30Warning for absolute name masking (making it deprecated, should becomeMatthieu Sozeau
2017-11-29Remove "obsolete_locality" and fix STM vernac classification.Maxime Dénès
2017-11-29Fix usage comment.Théo Zimmermann
2017-11-29This script apparently uses bash-specific features.Théo Zimmermann
2017-11-29Fix PR merge script.Théo Zimmermann
2017-11-29[lib] [api] Introduce record for `object_prefix`Emilio Jesus Gallego Arias
2017-11-29Forbid implicitly relative names in the checker.Pierre-Marie Pédrot
2017-11-29Mark the -I option in coqchk as deprecated and merge it with -Q.Pierre-Marie Pédrot
2017-11-29Add a -Q option to coqchck.Pierre-Marie Pédrot
2017-11-29[proof] [api] Rename proof types in preparation for functionalization.Emilio Jesus Gallego Arias
2017-11-29Merge PR #6271: Add PR backport script.Maxime Dénès
2017-11-29Merge PR #6253: Fixing inconsistent associativity of level 10 in the table of...Maxime Dénès
2017-11-29Merge PR #6199: [vernac] Uniformize type of vernac interpretation.Maxime Dénès
2017-11-29coq_makefile: pass filenames to coqchkRalf Jung
2017-11-29Documenting the possibility to pass filenames to coqchk.Pierre-Marie Pédrot
2017-11-29Allow to pass physical files to coqchk.Pierre-Marie Pédrot
2017-11-28In injection/inversion, consider all template-polymorphic types as injectable.Hugo Herbelin
2017-11-28use \ocaml macro in new textPaul Steckler
2017-11-28Adding a variant get_truncation_family_of of get_sort_family_of.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-28 12:06:30 +0000