aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.ml
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
|/
* Ad hoc fix for #5696, #7903 (ltac subterms and open subterms in notations).Gravatar Hugo Herbelin2018-06-26
* Remove reference name type.Gravatar Maxime Dénès2018-06-18
* [TYPO FIX] elimitate -> eliminateGravatar Siddharth2018-06-14
* [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Misctypes removal: miscellaneous aliases.Gravatar 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] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
* [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
* Fixing the 3 cases of a "Stream.Error" ended with two periods.Gravatar Hugo Herbelin2018-04-12
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
* Fix formatting of some ocamldoc comments to reduce warningsGravatar mrmr19932018-03-05
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-02-28
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
* Change default for notations with variables bound to both terms and binders.Gravatar Hugo Herbelin2018-02-20
* Notations: Adding modifiers to tell which kind of binder a constr can parse.Gravatar Hugo Herbelin2018-02-20
* Adding general support for irrefutable disjunctive patterns.Gravatar Hugo Herbelin2018-02-20
* Respecting the ident/pattern distinction in notation modifiers.Gravatar Hugo Herbelin2018-02-20
* Adding support for parsing subterms of a notation as "pattern".Gravatar Hugo Herbelin2018-02-20
* Adding patterns in the category of binders for notations.Gravatar Hugo Herbelin2018-02-20
* Preliminary work before extending support for binders in notationsGravatar Hugo Herbelin2018-02-20
* Make pattern variables of "match" substitutable in notations.Gravatar Hugo Herbelin2018-02-20
* Supporting recursive notations reversing the left-to-right order.Gravatar Hugo Herbelin2018-02-20
* Allowing variables used in recursive notation to occur several times in pattern.Gravatar Hugo Herbelin2018-02-20
* Allows recursive patterns for binders to be associative on the left.Gravatar Hugo Herbelin2018-02-20
* Fixing/improving notations with recursive patterns.Gravatar Hugo Herbelin2018-02-20
* Minor clarifying of name variables in constrintern.ml.Gravatar Hugo Herbelin2018-02-20
* Using name given by user to name a 'pat, if any.Gravatar Hugo Herbelin2018-02-20
* Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Gravatar Hugo Herbelin2018-02-20
* Notations: Do not consider a non-occurring variable as a binder-only variable.Gravatar Hugo Herbelin2018-02-20
* Again one more step in fixing #5762 ("where" clause).Gravatar Hugo Herbelin2018-02-20
* Merge PR #1047: Support universe instances on the literal TypeGravatar Maxime Dénès2018-02-12
|\
* | Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-01-30
| * Support universe instances on the literal TypeGravatar Tej Chajed2018-01-26
|/
* Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.Gravatar Maxime Dénès2017-12-18
|\
* \ Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml`Gravatar Maxime Dénès2017-12-15
|\ \
| | * [econstr] Switch constrintern API to non-imperative style.Gravatar Emilio Jesus Gallego Arias2017-12-15
| |/
| * [econstr] Cleanup in `vernac/classes.ml`.Gravatar Emilio Jesus Gallego Arias2017-12-13
* | Removing cumbersome location in multiple patterns.Gravatar Hugo Herbelin2017-12-12
|/
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-05 12:22:29 +0000