aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.ml
Commit message (Expand)AuthorAge
* [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
|/
* Merge PR #6185: [parser] Remove unnecessary statically initialized hook.Gravatar Maxime Dénès2017-11-21
|\
* \ Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 (clause...Gravatar Maxime Dénès2017-11-20
|\ \
| | * [parser] Remove unnecessary statically initialized hook.Gravatar Emilio Jesus Gallego Arias2017-11-19
| |/ |/|
| * One more step in fixing #5762 ("where" clause).Gravatar Hugo Herbelin2017-11-14
* | [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
|/
* Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...Gravatar Maxime Dénès2017-10-20
|\
| * Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).Gravatar Hugo Herbelin2017-10-05
* | Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
|/
* Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-09-04
* Remove understand_tcc_evars.Gravatar Maxime Dénès2017-08-01
* Fixing a little location bug with recursive binders.Gravatar Hugo Herbelin2017-07-18
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Merge PR#719: Constrexpr.Numeral without bigintGravatar Maxime Dénès2017-06-15
|\
| * Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Gravatar Pierre Letouzey2017-06-14
* | Remove support for Coq 8.2.Gravatar Guillaume Melquiond2017-06-14
|/
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 09:08:07 +0000