aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Expand)AuthorAge
* Merge PR #7941: Extend QuestionMark to produce a better error message in case...Gravatar Pierre-Marie Pédrot2018-07-19
|\
| * change into QuestionMark defaultGravatar Siddharth Bhat2018-07-17
| * Change QuestionMark for better record field missing error message.Gravatar Siddharth Bhat2018-07-17
* | [build] Build Coq and plugins with `-strict-sequence`Gravatar Emilio Jesus Gallego Arias2018-07-14
|/
* Merge PR #7080: Swapping Context and Constr and defining declarations on cons...Gravatar Maxime Dénès2018-06-29
|\
* \ Merge PR #7866: Implementation of mutual records in the higher strataGravatar Maxime Dénès2018-06-28
|\ \
| | * Swapping Context and Constr: defining declarations on constr in Constr.Gravatar Hugo Herbelin2018-06-27
| |/ |/|
* | Ad hoc fix for #5696, #7903 (ltac subterms and open subterms in notations).Gravatar Hugo Herbelin2018-06-26
| * Handle mutual records in upper layers.Gravatar Pierre-Marie Pédrot2018-06-24
|/
* Using more general information for primitive records.Gravatar Pierre-Marie Pédrot2018-06-23
* Merge PR #7797: Remove reference name type.Gravatar Enrico Tassi2018-06-19
|\
| * Remove reference name type.Gravatar Maxime Dénès2018-06-18
* | Remove the proj_eta field of the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
* | Remove special declaration of primitive projections in the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
|/
* [TYPO FIX] elimitate -> eliminateGravatar Siddharth2018-06-14
* [api] Remove Misctypes.Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Misctypes removal: move Tactypes to proofsGravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Misctypes removal: miscellaneous aliases.Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Misctypes removal: module_kind to DeclaremodsGravatar Emilio Jesus Gallego Arias2018-06-12
* Fixing #7700 (section variables bound to abbreviations were not found).Gravatar Hugo Herbelin2018-06-10
* Merge PR #7682: Fixes #7641: more detailed message about disjunctive patterns...Gravatar Emilio Jesus Gallego Arias2018-06-03
|\
| * Fixes #7641: more detailed message for disjunctive patterns with different vars.Gravatar Hugo Herbelin2018-06-03
* | Fixes #7636: location missing on deprecated compatibility notations.Gravatar Hugo Herbelin2018-06-02
|/
* [notations] Split interpretation and parsing of notationsGravatar Emilio Jesus Gallego Arias2018-05-31
* [api] Move `Constrexpr` to the `interp` module.Gravatar Emilio Jesus Gallego Arias2018-05-31
* [api] Remove deprecated objects in engine / interp / libraryGravatar Emilio Jesus Gallego Arias2018-05-30
* [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
* Remove some occurrences of Evd.emptyGravatar Maxime Dénès2018-05-25
* Merge PR #7177: Unifying names of "smart" combinators + adding combinators in...Gravatar Pierre-Marie Pédrot2018-05-24
|\
| * Moving Option.smart_map to Option.Smart.map.Gravatar Hugo Herbelin2018-05-23
| * Collecting List.smart_* functions into a module List.Smart.Gravatar Hugo Herbelin2018-05-23
| * Collecting Array.smart_* functions into a module Array.Smart.Gravatar Hugo Herbelin2018-05-23
* | [api] Move `Vernacexpr` to parsing.Gravatar Emilio Jesus Gallego Arias2018-05-23
|/
* Merge PR #7384: Split UniversesGravatar Pierre-Marie Pédrot2018-05-22
|\
* \ Merge PR #6965: [api] Move universe syntax to `Glob_term`Gravatar Pierre-Marie Pédrot2018-05-18
|\ \
| | * Split off Universes functions dealing with generating new universes.Gravatar Gaëtan Gilbert2018-05-17
| | * Split off Universes functions dealing with names.Gravatar Gaëtan Gilbert2018-05-17
| |/ |/|
* | Fixing a bug in printing the body of a located notation.Gravatar Hugo Herbelin2018-05-13
* | Removing a superfluous trailing newline in "Locate" for a notation.Gravatar Hugo Herbelin2018-05-13
* | Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).Gravatar Hugo Herbelin2018-05-10
* | Fixes part 1 of #7462 (only-printing not to override existing interp rule).Gravatar Hugo Herbelin2018-05-10
| * [api] Move universe syntax to `Glob_term`Gravatar Emilio Jesus Gallego Arias2018-05-08
|/
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* [api] Relocate `intf` modules according to dependency-order.Gravatar Emilio Jesus Gallego Arias2018-04-23
* Merge PR #7231: Fixing the 3 cases of a "Stream.Error" ended with two periods.Gravatar Enrico Tassi2018-04-13
|\
* \ Merge PR #6972: [api] Deprecate a couple of aliases that we missed.Gravatar Maxime Dénès2018-04-12
|\ \
| | * Fixing the 3 cases of a "Stream.Error" ended with two periods.Gravatar Hugo Herbelin2018-04-12
| |/ |/|
* | Merge PR #7116: Fixes #7110: missing test on the absence of a "as" while look...Gravatar Emilio Jesus Gallego Arias2018-04-09
|\ \
* \ \ Merge PR #7129: Fix #7124: Warning "Ignoring implicit status" does not provid...Gravatar Hugo Herbelin2018-04-06
|\ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-18 22:05:46 +0000