Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Merge PR #6381: A version of [time] that works on constr evaluation | 2017-12-18 | |
|\ | |||
* \ | Merge PR #6406: Make [abstract] nodes show up in the Ltac profile | 2017-12-18 | |
|\ \ | |||
* \ \ | Merge PR #6380: Add tactics to reset and display the Ltac profile | 2017-12-18 | |
|\ \ \ | |||
* \ \ \ | Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in Extra... | 2017-12-18 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #6411: Fix #5081 by more fine-grained LtacProf recording | 2017-12-18 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #6419: [vernac] Split `command.ml` into separate files. | 2017-12-18 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #6413: [econstr] Switch constrintern API to non-imperative style. | 2017-12-18 | |
|\ \ \ \ \ \ \ | |||
| | * | | | | | | [flags] Make program_mode a parameter for commands in vernac. | 2017-12-17 | |
| | * | | | | | | [vernac] Split `command.ml` into separate files. | 2017-12-17 | |
| |/ / / / / / | |||
* | | | | | | | Merge PR #6219: Document undocumented options | 2017-12-15 | |
|\ \ \ \ \ \ \ | |||
| | * | | | | | | [econstr] Switch constrintern API to non-imperative style. | 2017-12-15 | |
| | | | | | * | | Pass a ghost location for abstract | 2017-12-14 | |
| | | | | | * | | Make [abstract] nodes show up in the Ltac profile | 2017-12-14 | |
| |_|_|_|_|/ / |/| | | | | | | |||
| * | | | | | | Deprecate dead option Match Strict (ssr). | 2017-12-14 | |
| * | | | | | | Deprecate dead code option Congruence Depth. | 2017-12-14 | |
| | | | | | * | Add named timers to LtacProf | 2017-12-14 | |
| | | | | |/ | |||
| | | | | * | Add tactics to reset and display the Ltac profile | 2017-12-14 | |
| |_|_|_|/ |/| | | | | |||
* | | | | | Merge PR #6386: Catch errors while coercing 'and' intro patterns | 2017-12-14 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #6116: ssr: fill_occ_pattern: return valid ustate even if no match (... | 2017-12-14 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #6379: Fix profiling plugin | 2017-12-14 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #978: In printing, experimenting factorizing "match" clauses with sa... | 2017-12-14 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #6169: Clean up/deprecated options | 2017-12-14 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind. | 2017-12-14 | |
|\ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | * | | Fix #5081 by more fine-grained LtacProf recording | 2017-12-12 | |
| | | | | | | | |/ / | |||
| | | * | | | | | | | In printing, factorizing "match" clauses with same right-hand side. | 2017-12-12 | |
| | | * | | | | | | | Removing cumbersome location in multiple patterns. | 2017-12-12 | |
| | | | * | | | | | | Use msg_info for LtacProf | 2017-12-11 | |
| | | | * | | | | | | Allow LtacProf tactics to be called | 2017-12-11 | |
| | | | | |_|_|/ / | | | | |/| | | | | |||
| | | | | | * | | | Catch errors while coercing 'and' intro patterns | 2017-12-11 | |
| | | | | |/ / / | | | | |/| | | | |||
* | | | / | | | | [proof] Embed evar_map in RefinerError exception. | 2017-12-11 | |
| |_|_|/ / / / |/| | | | | | | |||
| | * | | | | | Remove deprecated appcontext and corresponding documentation. | 2017-12-11 | |
| | * | | | | | Remove deprecated option Tactic Compat Context. | 2017-12-11 | |
| |/ / / / / |/| | | | | | |||
* | | | | | | Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract. | 2017-12-11 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #1150: [stm] Remove all but one use of VtUnknown. | 2017-12-11 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #6338: Remove up-to-conversion term matching | 2017-12-11 | |
|\ \ \ \ \ \ \ \ | |_|_|_|/ / / / |/| | | | | | | | |||
| | | | * | | | | [lib] Rename Profile to CProfile | 2017-12-09 | |
| |_|_|/ / / / |/| | | | | | | |||
| | * | | | | | [stm] Remove all but one use of VtUnknown. | 2017-12-09 | |
| |/ / / / / |/| | | | | | |||
* | | | | | | Merge PR #6158: Allows a level in the raw and glob printers | 2017-12-08 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #6322: Fix #6286 (non stability of micromega csdp cache rebuilding) | 2017-12-07 | |
|\ \ \ \ \ \ \ | |||
| | | * | | | | | Getting rid of pf_is_matching in Funind. | 2017-12-06 | |
| |_|/ / / / / |/| | | | | | | |||
| | | | | | * | issue deprecation warning for "Ocaml" | 2017-12-06 | |
| | | * | | | | Fix #6323: stronger restrict universe context vs abstract. | 2017-12-06 | |
| |_|/ / / / |/| | | | | | |||
| * | | | | | Replacing Hashtbl.add by Hashtbl.replace in micromega cache building. | 2017-12-05 | |
| | | | | * | use \ocaml macro in Extraction chapter; accept OCaml in Extraction Language | 2017-12-05 | |
| |_|_|_|/ |/| | | | | |||
* | | | | | Merge PR #890: Global universe declarations | 2017-12-05 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212 | 2017-12-05 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #6210: More complete not-fully-applied error messages, #6145 | 2017-12-05 | |
|\ \ \ \ \ \ \ | |_|_|/ / / / |/| | | | | | | |||
| | | * | | | | Proper nametab handling of global universe names | 2017-12-01 | |
| |_|/ / / / |/| | | | | | |||
* | | | | | | Remove "obsolete_locality" and fix STM vernac classification. | 2017-11-29 | |
| |_|_|_|/ |/| | | | | |||
| * | | | | more complete not-fully-applied error messages, #6145 | 2017-11-28 |