aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
Commit message (Expand)AuthorAge
* 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
|/ / /
| * / Adding support for recursive notations of the form "x , .. , y , z".Gravatar Hugo Herbelin2017-07-26
|/ /
* | Merge PR #899: [general] Move files to directories so they match linking order.Gravatar Maxime Dénès2017-07-20
|\ \
* \ \ Merge branch 'v8.7'Gravatar Maxime Dénès2017-07-20
|\ \ \
* \ \ \ Merge PR #770: [proof] Move bullets to their own module.Gravatar Maxime Dénès2017-07-19
|\ \ \ \
| | | * | [general] Move files to directories matching linking order.Gravatar Emilio Jesus Gallego Arias2017-07-19
| |_|/ / |/| | |
* | | | Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layersGravatar Maxime Dénès2017-07-17
|\ \ \ \
* \ \ \ \ Merge PR #862: Adding support for bindings tags to explicit prefix/suffix rat...Gravatar Maxime Dénès2017-07-17
|\ \ \ \ \
| | * | | | Removing the uses of abstraction-breaking code in Lemmas.Gravatar Pierre-Marie Pédrot2017-07-13
| | * | | | Removing the uses of abstraction-breaking code in Obligations.Gravatar Pierre-Marie Pédrot2017-07-13
| | * | | | Remove the function Global.type_of_global_unsafe.Gravatar Pierre-Marie Pédrot2017-07-13
| | * | | | The only abstraction-breaking function in Univ is now AUContext.instance.Gravatar Pierre-Marie Pédrot2017-07-13
| | * | | | Getting rid of AUContext abstraction breakers in Discharge.Gravatar Pierre-Marie Pédrot2017-07-13
| | * | | | Make the typeclass implementation fully compatible with universe polymorphism.Gravatar Pierre-Marie Pédrot2017-07-13