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