Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | | | | * | | | | | | | Added a test for #4765 (an example of printing abbreviation with binders). | 2017-05-20 | ||
| |_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | ||||
| | | | | * | | | | | | | Deprecate -nodoc. | 2017-05-20 | ||
| | | | | | | | | | | * | [coqdoc] Add keywords in bug 2884. | 2017-05-20 | ||
| | * | | | | | | | | | | Change wrong bullet message. | 2017-05-20 | ||
| | | * | | | | | | | | | Revised behavior on ill-formed identifiers. | 2017-05-20 | ||
| |_|/ / / / / / / / / |/| | | | | | | | | | | ||||
* | | | | | | | | | | | Merge PR#276: Stopping injection not to work on discriminable atoms (see #4890). | 2017-05-20 | ||
|\ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | * | | | | | | | Mention ./configure in INSTALL.doc | 2017-05-20 | ||
| | | | |/ / / / / / / | | | |/| | | | | | | | ||||
* | | | | | | | | | | | Merge PR#654: Travis: do not cache opam logs (+prettier spacing) | 2017-05-20 | ||
|\ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR#643: [ide] Disable `print_ast` call. | 2017-05-20 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | ||||
* | | | | | | | | | | | | Merge PR#474: A fix for #5390 (a useful error on used introduction names was ... | 2017-05-20 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | * | | | | | | [test-suite] Add tests for goal printing. | 2017-05-20 | ||
* | | | | | | | | | | | | | Merge PR#627: Obligations shrinking: shrink abstraction too | 2017-05-20 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#644: [toplevel] [stm] Avoid edit_at in batch mode (bug #5520) | 2017-05-20 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | Merge PR#648: Allow interactive editing of `plugins/` by adding .dir-locals.el | 2017-05-20 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#649: Fix a typo | 2017-05-20 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#651: Re-adding explicit dependency of misc universe test into all_st... | 2017-05-20 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#640: [toplevel] Restore 8.6 goal printing behavior. | 2017-05-20 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | * | Exporting some functions of vars.ml as functions operating on EConstr. | 2017-05-19 | ||
| | | | | | | | | | | | | | | | * | In EConstr, defining some "cast" functions earlier. | 2017-05-19 | ||
| | | | | | | | | | | | | | | | * | Moving "sym" on "eq" type to lib/util.ml. | 2017-05-19 | ||
| | | | | | | | | * | | | | | | | | Travis: do not cache opam logs (+prettier spacing) | 2017-05-19 | ||
| |_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | ||||
| | * | | | | | | | | | | | | | | Re-adding explicit dependency of misc universe test into all_stdlib.v. | 2017-05-19 | ||
| |/ / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | ||||
| | | | | | | | | | * | | | | | Fixing an extra bug with pattern_of_constr. | 2017-05-19 | ||
| |_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | ||||
| | | | | | | | | | | * | | | Removing unused warnings. | 2017-05-19 | ||
| | | | | | | | | | | * | | | Merge branch 'master' into ltac2-hooks | 2017-05-19 | ||
| | | | | | | | | | | |\ \ \ | |_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | ||||
| | * | | | | | | | | | | | | Fix a typo | 2017-05-18 | ||
| |/ / / / / / / / / / / / |/| | | | | | | | | | | | | ||||
| | * | | | | | | | | | | | Add .dir-locals.el to plugins | 2017-05-18 | ||
| |/ / / / / / / / / / / |/| | | | | | | | | | | | ||||
| | | | | | | | | * | | | Adding a trespasser warning to the Nametab API. | 2017-05-18 | ||
| | | | | | | | | | * | | [stm] Tweak debug options. | 2017-05-18 | ||
| | * | | | | | | | | | | [toplevel] [stm] Avoid edit_at in batch mode (bug #5520) | 2017-05-18 | ||
| | | |_|_|_|_|_|_|/ / | | |/| | | | | | | | | ||||
| | | | | * | | | | | | [ide] Disable `print_ast` call. | 2017-05-18 | ||
| | | |_|/ / / / / / | | |/| | | | | | | | ||||
| | | | * | | | | | | A fix for #5390 (a useful error on used introduction names was masked). | 2017-05-17 | ||
| | | |/ / / / / / | | |/| | | | | | | ||||
* | | | | | | | | | Merge PR#633: An extension of EXTEND and notations to make standard parsing t... | 2017-05-17 | ||
|\ \ \ \ \ \ \ \ \ | |_|/ / / / / / / |/| | | | | | | | | ||||
| | | | * | | | | | Documenting relaxing of constraints on injection. | 2017-05-17 | ||
| | | | * | | | | | Stopping injection not to work on discriminable atoms (see #4890). | 2017-05-17 | ||
| |_|_|/ / / / / |/| | | | | | | | ||||
* | | | | | | | | Merge PR#457: Adding an even more compact goal hyps mode. | 2017-05-17 | ||
|\ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ | Merge PR#607: Make congruence reuse discriminate instead of rolling its own. | 2017-05-17 | ||
|\ \ \ \ \ \ \ \ \ | ||||
| | | | * | | | | | | [toplevel] Restore 8.6 goal printing behavior. | 2017-05-17 | ||
* | | | | | | | | | | Merge branch 'v8.6' | 2017-05-17 | ||
|\ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ | Merge PR#620: Reorganization of the layout for miscellaneous tests | 2017-05-17 | ||
|\ \ \ \ \ \ \ \ \ \ \ | | |_|_|_|_|_|_|_|_|/ | |/| | | | | | | | | | ||||
* | | | | | | | | | | | Merge PR#614: Improve Travis | 2017-05-17 | ||
|\ \ \ \ \ \ \ \ \ \ \ | ||||
| * | | | | | | | | | | | Travis: add -warn-error targets (standard and 4.04.1 ocaml) | 2017-05-17 | ||
* | | | | | | | | | | | | Merge PR#630: [interp] [ast] Make raw_cases_pattern_expr private + small cleanup | 2017-05-17 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | | | | | Travis: deduplicate package list for coqide+documentation targets | 2017-05-17 | ||
| | * | | | | | | | | | | | Travis: do not run the tests if building Coq fails | 2017-05-17 | ||
| |/ / / / / / / / / / / |/| | | | | | | | | | | | ||||
| | | * | | | | | | | | | Merge PR#635: Fixing #5522 (anomaly with free vars of pat) | 2017-05-17 | ||
| | | |\ \ \ \ \ \ \ \ \ | ||||
* | | | \ \ \ \ \ \ \ \ \ | Merge PR#636: Miscellaneous typos, dead code, etc. | 2017-05-17 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#639: Stop using auto with * in two proofs. | 2017-05-17 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | Stop using auto with * in two proofs. | 2017-05-16 | ||
|/ / / / / / / / / / / / / | ||||
| | | | | | | | * | | | | | Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND. | 2017-05-16 |