aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrextern.ml
Commit message (Expand)AuthorAge
* Remove reference name type.Gravatar Maxime Dénès2018-06-18
* [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
* Merge PR #7116: Fixes #7110: missing test on the absence of a "as" while look...Gravatar Emilio Jesus Gallego Arias2018-04-09
|\
* \ Merge PR #7127: Fix #6257: anomaly with Printing Projections and Context.Gravatar Hugo Herbelin2018-04-04
|\ \
| * | Fix #6257: anomaly with Printing Projections and Context.Gravatar Gaëtan Gilbert2018-03-30
| | * Fixes #7110 ("as" untested while looking for notation for nested patterns).Gravatar Hugo Herbelin2018-03-29
| |/
* / Patterns: Accepting patterns in PFix and PCofix and not only constr.Gravatar Hugo Herbelin2018-03-28
|/
* [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
* Revert "Merge PR #873: New strategy based on open scopes for deciding which n...Gravatar Maxime Dénès2018-03-09
* 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
* Adding general support for irrefutable disjunctive patterns.Gravatar Hugo Herbelin2018-02-20
* Using an "as" clause when needed for printing irrefutable patterns.Gravatar Hugo Herbelin2018-02-20
* Adding support for parsing subterms of a notation as "pattern".Gravatar Hugo Herbelin2018-02-20
* Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Gravatar Hugo Herbelin2018-02-20
* Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-01-30
* In printing, factorizing "match" clauses with same right-hand side.Gravatar Hugo Herbelin2017-12-12
* Removing cumbersome location in multiple patterns.Gravatar Hugo Herbelin2017-12-12
* Selecting which notation to print based on current stack of scope.Gravatar Hugo Herbelin2017-11-27
* Merge PR #6185: [parser] Remove unnecessary statically initialized hook.Gravatar Maxime Dénès2017-11-21
|\
| * [parser] Remove unnecessary statically initialized hook.Gravatar Emilio Jesus Gallego Arias2017-11-19
* | [lib] Minor pending cleanup to consolidate helper function.Gravatar Emilio Jesus Gallego Arias2017-11-19
|/
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Name.Id in core.Gravatar Emilio Jesus Gallego Arias2017-11-04
* Fixing #5401 (printing of patterns with bound anonymous variables).Gravatar Hugo Herbelin2017-10-28
* 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
* A little reorganization of notations + a fix to #5608.Gravatar Hugo Herbelin2017-08-29
* Detyping functions are now operating on EConstr.t.Gravatar Pierre-Marie Pédrot2017-08-01
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Merge PR#719: Constrexpr.Numeral without bigintGravatar Maxime Dénès2017-06-15
|\
* \ Merge PR#765: Remove obsolete Show commandsGravatar Maxime Dénès2017-06-14
|\ \
* | | [print] Allow Selective Printing of NotationsGravatar Emilio Jesus Gallego Arias2017-06-14
| | * Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Gravatar Pierre Letouzey2017-06-14
| |/ |/|
| * Remove more dead code (follow-up of previous commit).Gravatar Théo Zimmermann2017-06-12
|/
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\
* \ Merge PR#716: Don't double up on periods in anomaliesGravatar Maxime Dénès2017-06-06
|\ \
* \ \ Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...Gravatar Maxime Dénès2017-06-05
|\ \ \
| | * | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| |/ / |/| |
| * | Using a more explicit algebraic type for evars of kind "MatchingVar".Gravatar Hugo Herbelin2017-05-31
* | | Creating a module Nameops.Name extending module Names.Name.Gravatar Hugo Herbelin2017-05-31
|/ /
* | Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\ \
| * | [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| * | Revert "Using a more explicit algebraic type for evars of kind "MatchingVar"."Gravatar Maxime Dénès2017-04-28
| * | Using a more explicit algebraic type for evars of kind "MatchingVar".Gravatar Hugo Herbelin2017-04-28
* | | [location] [ast] Port module AST to CAstGravatar Emilio Jesus Gallego Arias2017-04-25
* | | [location] [ast] Switch Constrexpr AST to an extensible node type.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-05 18:53:36 +0000