Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Merge PR #6293: Check for Num lib if OCaml >= 4.06, fixes #6162 | 2017-12-05 | |
|\ | |||
* \ | Merge PR #6302: Uninstall doc dir, not dev (which is not installed), fixes #6007 | 2017-12-05 | |
|\ \ | |||
* \ \ | Merge PR #6287: Add merlin to default.nix | 2017-12-05 | |
|\ \ \ | |||
* \ \ \ | Merge PR #6210: More complete not-fully-applied error messages, #6145 | 2017-12-05 | |
|\ \ \ \ | |||
| | | * | | uninstall doc dir, not dev (which is not installed), #6007 | 2017-12-01 | |
| |_|/ / |/| | | | |||
| | | * | check for Num lib if OCaml >= 4.06, #6162 | 2017-12-01 | |
* | | | | Merge PR #736: [ci] Test coqchk on the CompCert target. | 2017-12-01 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #6256: CI: better ocaml warning checks | 2017-12-01 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #6276: Coqchk accepts filenames | 2017-12-01 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #6233: [proof] [api] Rename proof types in preparation for functiona... | 2017-12-01 | |
|\ \ \ \ \ \ \ | |_|_|_|_|_|/ |/| | | | | | | |||
* | | | | | | | Merge PR #1049: Remove obsolete locality | 2017-11-30 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #6244: [lib] [api] Introduce record for `object_prefix` | 2017-11-30 | |
|\ \ \ \ \ \ \ \ | |||
| | | | | | * | | | [ci] Test coqchk on the CompCert target. | 2017-11-30 | |
* | | | | | | | | | Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ... | 2017-11-30 | |
|\ \ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / / |/| | | | | | | | | |||
| | | | | | | | * | Add merlin in the dependencies of nix-shell only. | 2017-11-30 | |
| |_|_|_|_|_|_|/ |/| | | | | | | | |||
* | | | | | | | | Merge PR #6269: [ci] [vst] Shorten compilation time to avoid Travis timeouts. | 2017-11-30 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #6193: Fix (partial) #4878: option to stop autodeclaring axiom as in... | 2017-11-30 | |
|\ \ \ \ \ \ \ \ \ | |||
| | | | | * | | | | | Remove "obsolete_locality" and fix STM vernac classification. | 2017-11-29 | |
| |_|_|_|/ / / / / |/| | | | | | | | | |||
| | | | * | | | | | [lib] [api] Introduce record for `object_prefix` | 2017-11-29 | |
| | | | | * | | | | [proof] [api] Rename proof types in preparation for functionalization. | 2017-11-29 | |
| |_|_|_|/ / / / |/| | | | | | | | |||
* | | | | | | | | Merge PR #6271: Add PR backport script. | 2017-11-29 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #6253: Fixing inconsistent associativity of level 10 in the table of... | 2017-11-29 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #6199: [vernac] Uniformize type of vernac interpretation. | 2017-11-29 | |
|\ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | * | | | coq_makefile: pass filenames to coqchk | 2017-11-29 | |
| | | | | | | | * | | | Documenting the possibility to pass filenames to coqchk. | 2017-11-29 | |
| | | | | | | | * | | | Allow to pass physical files to coqchk. | 2017-11-29 | |
| | | | | | * | | | | | In injection/inversion, consider all template-polymorphic types as injectable. | 2017-11-28 | |
| | | | | | * | | | | | Adding a variant get_truncation_family_of of get_sort_family_of. | 2017-11-28 | |
| | | | | | * | | | | | Moving non-recursive function sort_family_of out of the retype block of recur... | 2017-11-28 | |
| | | | | | |/ / / / | |||
| | | | | | | * / / | Adding an interface file for checker/check.ml. | 2017-11-28 | |
| |_|_|_|_|_|/ / / |/| | | | | | | | | |||
| | | | | | | | * | more complete not-fully-applied error messages, #6145 | 2017-11-28 | |
| | | * | | | | | | Add PR backport script. | 2017-11-28 | |
| |_|/ / / / / / |/| | | | | | | | |||
| | | | * | | | | [ci] [vst] Shorten compilation time to avoid Travis timeouts. | 2017-11-28 | |
| |_|_|/ / / / |/| | | | | | | |||
| | | | | * | | CI: use -byte-only in [warnings] jobs. | 2017-11-28 | |
| | | | | * | | Fix native compute for byte compiled Coq. | 2017-11-28 | |
| | | * | | | | Fix (partial) #4878: option to stop autodeclaring axiom as instance. | 2017-11-28 | |
| |_|/ / / / |/| | | | | | |||
| | | | * | | Travis: do not build stdlib in [warnings] jobs. | 2017-11-28 | |
| |_|_|/ / |/| | | | | |||
* | | | | | Merge PR #6259: Add PR merge script. | 2017-11-28 | |
|\ \ \ \ \ | |||
| * | | | | | Add PR merge script. | 2017-11-28 | |
* | | | | | | Merge PR #1033: Universe binder improvements | 2017-11-28 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #6235: Fixing failing mkdir in test-suite for coq-makefile. | 2017-11-28 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #6248: [api] Remove aliases of `Evar.t` | 2017-11-28 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #6246: Ref. Man.: Updating the current official writing of OCaml; up... | 2017-11-28 | |
|\ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|/ / |/| | | | | | | | | |||
| | | | | | * | | | [vernac] Adjust `interp` to pass polymorphic in the attributes. | 2017-11-27 | |
| | | | | | * | | | [vernac] Add polymorphic to the type of vernac interpration options. | 2017-11-27 | |
| | | | | | * | | | [vernac] Start to uniformize type of vernac interpretation. | 2017-11-27 | |
| |_|_|_|_|/ / / |/| | | | | | | | |||
* | | | | | | | | Merge PR #6237: coq_makefile tests: build in easily removed temporary subdire... | 2017-11-27 | |
|\ \ \ \ \ \ \ \ | |_|_|_|_|/ / / |/| | | | | | | | |||
* | | | | | | | | Merge PR #6242: Use Evarutil.has_undefined_evars for tactic has_evar. | 2017-11-27 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #6236: Fix coq-makefile ocamldoc call when configured with -annotate. | 2017-11-27 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #6207: [stm] Allow delayed constant in interactive mode. | 2017-11-27 | |
|\ \ \ \ \ \ \ \ \ \ |