aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Expand)Author
2017-11-13Merge PR #6052: [general] Move Tactypes to `interp` + API reordering.Maxime Dénès
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-11-04[api] Deprecate all legacy uses of Name.Id in core.Emilio Jesus Gallego Arias
2017-11-03Merge PR #6051: Fix FIXME: use OCaml 4.02 generative functors when available.Maxime Dénès
2017-11-03Merge PR #6047: A generic printer for ltac valuesMaxime Dénès
2017-11-02Do not identify a pre_ident as a string Ltac value.Hugo Herbelin
2017-11-01[general] Move Tactypes to `interp`Emilio Jesus Gallego Arias
2017-11-01Fix FIXME: use OCaml 4.02 generative functors when available.Gaëtan Gilbert
2017-10-28Fixing #5401 (printing of patterns with bound anonymous variables).Hugo Herbelin
2017-10-25[general] Remove Econstr dependency from `intf`Emilio Jesus Gallego Arias
2017-10-20Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...Maxime Dénès
2017-10-09[deps] Move `Discharge` to `interp`Emilio Jesus Gallego Arias
2017-10-05Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).Hugo Herbelin
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-19Allow declaring universe constraints at definition level.Matthieu Sozeau
2017-09-18Reporting locations in error messages about notation formats.Hugo Herbelin
2017-09-15Merge PR #1037: Parse directly to Sorts.family when appropriate.Maxime Dénès
2017-09-12Adding a missing period in a notation warning.Hugo Herbelin
2017-09-12Fixing bugs of a67bd7f9 and c6d9d4fb in recognizing a 'pat binding.Hugo Herbelin
2017-09-12Fixing a typo in printing notations with recursive binders.Hugo Herbelin
2017-09-12Fixing a bug of recursive notations introduced in dfdaf4de.Hugo Herbelin
2017-09-12Fixing little inaccuracy in coercions to ident or name.Hugo Herbelin
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-29Merge PR #946: Functional pretyping interfaceMaxime Dénès
2017-08-29Merge PR #916: Fixing notation bug 5608 involving { } and a slight restructur...Maxime Dénès
2017-08-29Merge PR #773: [flags] Remove XML output flag.Maxime Dénès
2017-08-29A new step of restructuration of notations.Hugo Herbelin
2017-08-29A little reorganization of notations + a fix to #5608.Hugo Herbelin
2017-08-29Adapting code to renaming Array.fold_map -> Array.fold_left_map.Hugo Herbelin
2017-08-29Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_mapHugo Herbelin
2017-08-01[flags] Remove XML output flag.Emilio Jesus Gallego Arias
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-07-31Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadMaxime Dénès
2017-07-28Merge PR #889: Removing template polymorphism for definitions.Maxime Dénès
2017-07-28Merge PR #888: Stronger kernel typesMaxime Dénès
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-26Removing template polymorphism for definitions.Pierre-Marie Pédrot
2017-07-26Merge PR #894: Fixing a little location bug with recursive bindersMaxime Dénès
2017-07-26Further simplication: do not recreate entries for side-effects.Pierre-Marie Pédrot
2017-07-26Remove a horrendous hack in Declare to retrieve exported side-effects.Pierre-Marie Pédrot
2017-07-26More precise type of entries capturing their lack of side-effects.Pierre-Marie Pédrot
2017-07-26More precise type for universe entries.Pierre-Marie Pédrot
2017-07-19[general] Move files to directories matching linking order.Emilio Jesus Gallego Arias
2017-07-18Fixing a little location bug with recursive binders.Hugo Herbelin
2017-07-13Remove the function Global.type_of_global_unsafe.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 00:37:57 +0000