aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Expand)Author
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
2018-06-26Ad hoc fix for #5696, #7903 (ltac subterms and open subterms in notations).Hugo Herbelin
2018-06-24Share the role type between the implementations of side-effects.Pierre-Marie Pédrot
2018-06-24Handle mutual records in upper layers.Pierre-Marie Pédrot
2018-06-23Using more general information for primitive records.Pierre-Marie Pédrot
2018-06-19Merge PR #7797: Remove reference name type.Enrico Tassi
2018-06-18Remove reference name type.Maxime Dénès
2018-06-17Remove the proj_eta field of the kernel.Pierre-Marie Pédrot
2018-06-17Remove special declaration of primitive projections in the kernel.Pierre-Marie Pédrot
2018-06-14[TYPO FIX] elimitate -> eliminateSiddharth
2018-06-12[api] Remove Misctypes.Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: move Tactypes to proofsEmilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: miscellaneous aliases.Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: module_kind to DeclaremodsEmilio Jesus Gallego Arias
2018-06-10Fixing #7700 (section variables bound to abbreviations were not found).Hugo Herbelin
2018-06-03Merge PR #7682: Fixes #7641: more detailed message about disjunctive patterns...Emilio Jesus Gallego Arias
2018-06-03Fixes #7641: more detailed message for disjunctive patterns with different vars.Hugo Herbelin
2018-06-02Fixes #7636: location missing on deprecated compatibility notations.Hugo Herbelin
2018-05-31[notations] Split interpretation and parsing of notationsEmilio Jesus Gallego Arias
2018-05-31[api] Move `Constrexpr` to the `interp` module.Emilio Jesus Gallego Arias
2018-05-30[api] Remove deprecated objects in engine / interp / libraryEmilio Jesus Gallego Arias
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
2018-05-25Remove some occurrences of Evd.emptyMaxime Dénès
2018-05-24Merge PR #7177: Unifying names of "smart" combinators + adding combinators in...Pierre-Marie Pédrot
2018-05-23Moving Option.smart_map to Option.Smart.map.Hugo Herbelin
2018-05-23Collecting List.smart_* functions into a module List.Smart.Hugo Herbelin
2018-05-23Collecting Array.smart_* functions into a module Array.Smart.Hugo Herbelin
2018-05-23[api] Move `Vernacexpr` to parsing.Emilio Jesus Gallego Arias
2018-05-22Merge PR #7384: Split UniversesPierre-Marie Pédrot
2018-05-18Merge PR #6965: [api] Move universe syntax to `Glob_term`Pierre-Marie Pédrot
2018-05-17Split off Universes functions dealing with generating new universes.Gaëtan Gilbert
2018-05-17Split off Universes functions dealing with names.Gaëtan Gilbert
2018-05-13Fixing a bug in printing the body of a located notation.Hugo Herbelin
2018-05-13Removing a superfluous trailing newline in "Locate" for a notation.Hugo Herbelin
2018-05-10Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).Hugo Herbelin
2018-05-10Fixes part 1 of #7462 (only-printing not to override existing interp rule).Hugo Herbelin
2018-05-08[api] Move universe syntax to `Glob_term`Emilio Jesus Gallego Arias
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-04-23[api] Relocate `intf` modules according to dependency-order.Emilio Jesus Gallego Arias
2018-04-13Merge PR #7231: Fixing the 3 cases of a "Stream.Error" ended with two periods.Enrico Tassi
2018-04-12Merge PR #6972: [api] Deprecate a couple of aliases that we missed.Maxime Dénès
2018-04-12Fixing the 3 cases of a "Stream.Error" ended with two periods.Hugo Herbelin
2018-04-09Merge PR #7116: Fixes #7110: missing test on the absence of a "as" while look...Emilio Jesus Gallego Arias
2018-04-06Merge PR #7129: Fix #7124: Warning "Ignoring implicit status" does not provid...Hugo Herbelin
2018-04-05Refactor impargs code.Jasper Hugunin
2018-04-05Fix #7124: Warning "Ignoring implicit status" does not provide line numberMaxime Dénès
2018-04-04Merge PR #7127: Fix #6257: anomaly with Printing Projections and Context.Hugo Herbelin
2018-03-30Fix #6257: anomaly with Printing Projections and Context.Gaëtan Gilbert
2018-03-29Fixes #7110 ("as" untested while looking for notation for nested patterns).Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 15:16:33 +0000