aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Expand)Author
2017-11-24Use Maps and ids for universe bindersGaëtan Gilbert
2017-11-24Use type Universes.universe_binders.Gaëtan Gilbert
2017-11-24Merge PR #486: Make some functions on terms more robust w.r.t new term constr...Maxime Dénès
2017-11-23Make some functions on terms more robust w.r.t new term constructs.Maxime Dénès
2017-11-22[api] Deprecate Term destructors, move to ConstrEmilio Jesus Gallego Arias
2017-11-21[printing] Deprecate all printing functions accessing the global proof.Emilio Jesus Gallego Arias
2017-11-21Merge PR #6185: [parser] Remove unnecessary statically initialized hook.Maxime Dénès
2017-11-20Merge PR #6184: [lib] Minor pending cleanup to consolidate helper function.Maxime Dénès
2017-11-20Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 (clause...Maxime Dénès
2017-11-19[parser] Remove unnecessary statically initialized hook.Emilio Jesus Gallego Arias
2017-11-19[lib] Minor pending cleanup to consolidate helper function.Emilio Jesus Gallego Arias
2017-11-14One more step in fixing #5762 ("where" clause).Hugo Herbelin
2017-11-13[api] Another large deprecation, `Nameops`Emilio Jesus Gallego Arias
2017-11-13Merge PR #6098: [api] Move structures deprecated in the API to the core.Maxime Dénès
2017-11-13Merge PR #6065: [api] Deprecate all legacy uses of Names in core.Maxime Dénès
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 14:47:03 +0000