| Commit message (Expand) | Author | Age |
... | |
* | | | | | Merge PR #1040: Efficient fresh name generation | Maxime Dénès | 2017-10-03 |
|\ \ \ \ \ |
|
* | | | | | | [vernac] Remove `Qed exporting` syntax. | Emilio Jesus Gallego Arias | 2017-09-29 |
| |_|_|/ /
|/| | | | |
|
| * | | | | Efficient fresh name generation relying on sets. | Pierre-Marie Pédrot | 2017-09-28 |
|/ / / / |
|
* | | | | Merge PR #688: Binding universe constraints in Definition/Inductive/etc... | Maxime Dénès | 2017-09-26 |
|\ \ \ \ |
|
| | | | * | BZ#5739, Allow level for leftmost nonterminal for printing-ony Notations | Paul Steckler | 2017-09-25 |
* | | | | | Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ... | Maxime Dénès | 2017-09-25 |
|\ \ \ \ \ |
|
* \ \ \ \ \ | Merge PR #1057: Reporting locations in error messages about notation formats. | Maxime Dénès | 2017-09-25 |
|\ \ \ \ \ \ |
|
| | * | | | | | Discharge.ml: cosmetic renaming of some variables. | Hugo Herbelin | 2017-09-23 |
| | * | | | | | Fixing #5755 (discharging of inductive types not correct with let-ins). | Hugo Herbelin | 2017-09-23 |
| |/ / / / /
|/| | | | | |
|
| | | | * | | Himsg: Dropping nf_evars made obsolete by EConstr. | Hugo Herbelin | 2017-09-22 |
| | | | * | | Cannot unify message: improve preventing repeating twice the same message. | Hugo Herbelin | 2017-09-22 |
| | | | |/ |
|
* | | | | | Merge PR #1055: Remove STM vernaculars | Maxime Dénès | 2017-09-22 |
|\ \ \ \ \ |
|
* | | | | | | [flags] Flag `open Flags` | Emilio Jesus Gallego Arias | 2017-09-20 |
| |_|_|_|/
|/| | | | |
|
| * | | | | Remove STM vernaculars. | Maxime Dénès | 2017-09-19 |
|/ / / / |
|
| | * | | Don't lose names in UState.universe_context. | Gaëtan Gilbert | 2017-09-19 |
| | * | | proof_global: cleanup and comment close_proof | Matthieu Sozeau | 2017-09-19 |
| | * | | Allow declaring universe constraints at definition level. | Matthieu Sozeau | 2017-09-19 |
| |/ /
|/| | |
|
| * | | Reporting locations in error messages about notation formats. | Hugo Herbelin | 2017-09-18 |
| * | | Fixing two anomalies in corner cases of the syntax of notation formats. | Hugo Herbelin | 2017-09-18 |
|/ / |
|
* | | Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ... | Maxime Dénès | 2017-09-15 |
|\ \ |
|
* \ \ | Merge PR #1051: Using an algebraic type for distinguishing toplevel input fro... | Maxime Dénès | 2017-09-15 |
|\ \ \ |
|
* \ \ \ | Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already. | Maxime Dénès | 2017-09-15 |
|\ \ \ \ |
|
* \ \ \ \ | Merge PR #1037: Parse directly to Sorts.family when appropriate. | Maxime Dénès | 2017-09-15 |
|\ \ \ \ \ |
|
* \ \ \ \ \ | Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" In... | Maxime Dénès | 2017-09-15 |
|\ \ \ \ \ \ |
|
| | | | * | | | Using an algebraic type for distinguishing toplevel input from location in file. | Hugo Herbelin | 2017-09-14 |
| |_|_|/ / /
|/| | | | | |
|
| | | | | * | A possible fix for BZ#5715 (escape non-utf8 win32 file names). | Hugo Herbelin | 2017-09-13 |
* | | | | | | Fixing bug #5693 (treating empty notation format as any format). | Hugo Herbelin | 2017-09-12 |
| |_|_|_|/
|/| | | | |
|
| | | * | | Port is_Set and is_Type to EConstr, as was is_Prop already. | Guillaume Melquiond | 2017-09-12 |
| |_|/ /
|/| | | |
|
| | * | | Parse directly to Sorts.family when appropriate. | Gaëtan Gilbert | 2017-09-08 |
| |/ /
|/| | |
|
* | | | Making detyping potentially lazy. | Pierre-Marie Pédrot | 2017-09-04 |
* | | | Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name | Maxime Dénès | 2017-08-31 |
|\ \ \ |
|
| | * | | Fixing a capitalization in the middle of the sentence of an error message. | Hugo Herbelin | 2017-08-30 |
| | | * | [vernac] Store Infix Modifier in Vernac Notation. | Pierre-Marie Pédrot | 2017-08-29 |
| |_|/
|/| | |
|
* | | | Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170 | Maxime Dénès | 2017-08-29 |
|\ \ \ |
|
* \ \ \ | Merge PR #946: Functional pretyping interface | Maxime Dénès | 2017-08-29 |
|\ \ \ \ |
|
* | | | | | Quoting notations in incompatible-level error message. | Hugo Herbelin | 2017-08-29 |
* | | | | | A new step of restructuration of notations. | Hugo Herbelin | 2017-08-29 |
* | | | | | Dropping former fix to bug #5469 (notation format not recognizing curly braces). | Hugo Herbelin | 2017-08-29 |
* | | | | | A little reorganization of notations + a fix to #5608. | Hugo Herbelin | 2017-08-29 |
| |_|_|/
|/| | | |
|
| | | * | Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_map | Hugo Herbelin | 2017-08-29 |
| |_|/
|/| | |
|
| | * | Add native compute profiling, BZ#5170 | Paul Steckler | 2017-08-17 |
| |/
|/| |
|
* | | Merge PR #912: Detyping functions are now operating on EConstr.t. | Maxime Dénès | 2017-08-16 |
|\ \ |
|
* \ \ | Merge PR #841: Timorous fix of bug #5598 on global existing class in sections | Maxime Dénès | 2017-08-16 |
|\ \ \ |
|
* \ \ \ | Merge PR #864: Some cleanups after cumulativity for inductive types | Maxime Dénès | 2017-08-16 |
|\ \ \ \ |
|
| | | | * | Remove understand_tcc_evars. | Maxime Dénès | 2017-08-01 |
| |_|_|/
|/| | | |
|
| | | * | Detyping functions are now operating on EConstr.t. | Pierre-Marie Pédrot | 2017-08-01 |
| |_|/
|/| | |
|
* | | | Merge PR #919: Remove a few useless evar-normalizations in printing code. | Maxime Dénès | 2017-08-01 |
|\ \ \ |
|
* \ \ \ | Merge PR #834: Adding support for recursive notations of the form "x , .. , y... | Maxime Dénès | 2017-08-01 |
|\ \ \ \ |
|
| | | * | | Improve errors for cumulativity when monomorphic | Amin Timany | 2017-07-31 |
| | | * | | Change the option for cumulativity | Amin Timany | 2017-07-31 |