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