aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
Commit message (Expand)AuthorAge
* Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Gravatar Maxime Dénès2017-09-26
|\
* \ Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ...Gravatar Maxime Dénès2017-09-25
|\ \
* \ \ Merge PR #1057: Reporting locations in error messages about notation formats.Gravatar Maxime Dénès2017-09-25
|\ \ \
| | * | Discharge.ml: cosmetic renaming of some variables.Gravatar Hugo Herbelin2017-09-23
| | * | Fixing #5755 (discharging of inductive types not correct with let-ins).Gravatar Hugo Herbelin2017-09-23
| |/ / |/| |
* | | Merge PR #1055: Remove STM vernacularsGravatar Maxime Dénès2017-09-22
|\ \ \
* | | | [flags] Flag `open Flags`Gravatar Emilio Jesus Gallego Arias2017-09-20
| * | | Remove STM vernaculars.Gravatar Maxime Dénès2017-09-19
|/ / /
| | * Don't lose names in UState.universe_context.Gravatar Gaëtan Gilbert2017-09-19
| | * proof_global: cleanup and comment close_proofGravatar Matthieu Sozeau2017-09-19
| | * Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
| |/ |/|
| * Reporting locations in error messages about notation formats.Gravatar Hugo Herbelin2017-09-18
| * Fixing two anomalies in corner cases of the syntax of notation formats.Gravatar Hugo Herbelin2017-09-18
|/
* Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ...Gravatar Maxime Dénès2017-09-15
|\
* \ Merge PR #1051: Using an algebraic type for distinguishing toplevel input fro...Gravatar Maxime Dénès2017-09-15
|\ \
* \ \ Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.Gravatar Maxime Dénès2017-09-15
|\ \ \
* \ \ \ Merge PR #1037: Parse directly to Sorts.family when appropriate.Gravatar Maxime Dénès2017-09-15
|\ \ \ \
* \ \ \ \ Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" In...Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \
| | | | * | Using an algebraic type for distinguishing toplevel input from location in file.Gravatar Hugo Herbelin2017-09-14
| |_|_|/ / |/| | | |
* | | | | Fixing bug #5693 (treating empty notation format as any format).Gravatar Hugo Herbelin2017-09-12
| | | * | Port is_Set and is_Type to EConstr, as was is_Prop already.Gravatar Guillaume Melquiond2017-09-12
| |_|/ / |/| | |
| | * | Parse directly to Sorts.family when appropriate.Gravatar Gaëtan Gilbert2017-09-08
| |/ / |/| |
* | | Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-09-04
* | | Merge PR #980: Adding combinators + a canonical renaming in List, Option, NameGravatar Maxime Dénès2017-08-31
|\ \ \
| | * | Fixing a capitalization in the middle of the sentence of an error message.Gravatar Hugo Herbelin2017-08-30
| | | * [vernac] Store Infix Modifier in Vernac Notation.Gravatar Pierre-Marie Pédrot2017-08-29
| |_|/ |/| |
* | | Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170Gravatar Maxime Dénès2017-08-29
|\ \ \
* \ \ \ Merge PR #946: Functional pretyping interfaceGravatar Maxime Dénès2017-08-29
|\ \ \ \
* | | | | Quoting notations in incompatible-level error message.Gravatar Hugo Herbelin2017-08-29
* | | | | A new step of restructuration of notations.Gravatar Hugo Herbelin2017-08-29
* | | | | Dropping former fix to bug #5469 (notation format not recognizing curly braces).Gravatar Hugo Herbelin2017-08-29
* | | | | A little reorganization of notations + a fix to #5608.Gravatar Hugo Herbelin2017-08-29
| |_|_|/ |/| | |
| | | * Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_mapGravatar Hugo Herbelin2017-08-29
| |_|/ |/| |
| | * Add native compute profiling, BZ#5170Gravatar Paul Steckler2017-08-17
| |/ |/|
* | Merge PR #912: Detyping functions are now operating on EConstr.t.Gravatar Maxime Dénès2017-08-16
|\ \
* \ \ Merge PR #841: Timorous fix of bug #5598 on global existing class in sectionsGravatar Maxime Dénès2017-08-16
|\ \ \
* \ \ \ Merge PR #864: Some cleanups after cumulativity for inductive typesGravatar Maxime Dénès2017-08-16
|\ \ \ \
| | | | * Remove understand_tcc_evars.Gravatar Maxime Dénès2017-08-01
| |_|_|/ |/| | |
| | | * Detyping functions are now operating on EConstr.t.Gravatar Pierre-Marie Pédrot2017-08-01
| |_|/ |/| |
* | | Merge PR #919: Remove a few useless evar-normalizations in printing code.Gravatar Maxime Dénès2017-08-01
|\ \ \
* \ \ \ Merge PR #834: Adding support for recursive notations of the form "x , .. , y...Gravatar Maxime Dénès2017-08-01
|\ \ \ \
| | | * | Improve errors for cumulativity when monomorphicGravatar Amin Timany2017-07-31
| | | * | Change the option for cumulativityGravatar Amin Timany2017-07-31
| | | * | Issue error on monomorphic cumulative inductivesGravatar Amin Timany2017-07-31
* | | | | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\ \ \ \ \ | |_|_|/ / |/| | | |
| * | | | deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| | | * | Remove a few useless evar-normalizations in printing code.Gravatar Pierre-Marie Pédrot2017-07-26
| | |/ / | |/| |
* | | | Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
* | | | Statically ensuring that inlined entries out of the kernel have no effects.Gravatar Pierre-Marie Pédrot2017-07-26
* | | | More precise type for universe entries.Gravatar Pierre-Marie Pédrot2017-07-26
|/ / /
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 13:02:17 +0000