aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-12-11Fix anomaly in [Type foo] command, + print uctx like Check.Gaëtan Gilbert
2017-12-07Merge PR #6290: Rename update to set, Fixes #6196Maxime Dénès
2017-12-07Merge PR #873: New strategy based on open scopes for deciding which notation ...Maxime Dénès
2017-12-07Merge PR #6142: Single quotes break on WindowsMaxime Dénès
2017-12-07Merge PR #6277: Qualified import in coqchkMaxime Dénès
2017-12-07Merge PR #6322: Fix #6286 (non stability of micromega csdp cache rebuilding)Maxime Dénès
2017-12-07Merge PR #6321: Use preference for ocamlfind in configureMaxime Dénès
2017-12-07Merge PR #6316: Correct typoMaxime Dénès
2017-12-07Merge PR #6309: [default.nix] needs ncurses for the test-suiteMaxime Dénès
2017-12-07Merge PR #6303: Remove redundant Zcase from the checker.Maxime Dénès
2017-12-05Replacing Hashtbl.add by Hashtbl.replace in micromega cache building.Hugo Herbelin
2017-12-05Rename update to set, fixes #6196Paul Steckler
2017-12-05use preference for ocamlfindPaul Steckler
2017-12-05Correct typoMartin Vassor
2017-12-05[default.nix] explain ncurses dependencyVincent Laporte
2017-12-05Merge PR #890: Global universe declarationsMaxime Dénès
2017-12-05Merge PR #6266: Safe unmarshalling in the checkerMaxime Dénès
2017-12-05Merge PR #6301: [vernac] Couple of tweaks missing from previous PRs.Maxime Dénès
2017-12-05Merge PR #6306: Adding a test for #6304 (a bug with "fix" in notations).Maxime Dénès
2017-12-05Merge PR #6300: Clarify operation of sequences, fixes #6095Maxime Dénès
2017-12-05Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212Maxime Dénès
2017-12-05Merge PR #6293: Check for Num lib if OCaml >= 4.06, fixes #6162Maxime Dénès
2017-12-05Merge PR #6302: Uninstall doc dir, not dev (which is not installed), fixes #6007Maxime Dénès
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[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-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-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-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-29Remove "obsolete_locality" and fix STM vernac classification.Maxime Dénès