aboutsummaryrefslogtreecommitdiff
path: root/interp/constrextern.ml
AgeCommit message (Expand)Author
2018-11-20Notations: Trying using a notation with or w/o removal of coercions.Hugo Herbelin
2018-10-31Notations: fixing a bug with abbreviations in custom entries.Hugo Herbelin
2018-10-18[api] Qualify access to `Nametab`Emilio Jesus Gallego Arias
2018-10-02Revert #6651: Use r.(p) syntax to print primitive projectionsMaxime Dénès
2018-09-23Checking if low-level name printers are used on purpose or not.Hugo Herbelin
2018-08-31Notation: remove support for prim tokens denoting inductive types in "return"Pierre Letouzey
2018-07-29Adding support for custom entries in notations.Hugo Herbelin
2018-06-18Remove reference name type.Maxime Dénès
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
2018-04-09Merge PR #7116: Fixes #7110: missing test on the absence of a "as" while look...Emilio Jesus Gallego Arias
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
2018-03-28Patterns: Accepting patterns in PFix and PCofix and not only constr.Hugo Herbelin
2018-03-09[located] Push inner locations in `reference` to a CAst.t node.Emilio Jesus Gallego Arias
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-03-09Revert "Merge PR #873: New strategy based on open scopes for deciding which n...Maxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2018-02-20Adding general support for irrefutable disjunctive patterns.Hugo Herbelin
2018-02-20Using an "as" clause when needed for printing irrefutable patterns.Hugo Herbelin
2018-02-20Adding support for parsing subterms of a notation as "pattern".Hugo Herbelin
2018-02-20Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Hugo Herbelin
2018-01-30Use r.(p) syntax to print primitive projections.Maxime Dénès
2017-12-12In printing, factorizing "match" clauses with same right-hand side.Hugo Herbelin
2017-12-12Removing cumbersome location in multiple patterns.Hugo Herbelin
2017-11-27Selecting which notation to print based on current stack of scope.Hugo Herbelin
2017-11-21Merge PR #6185: [parser] Remove unnecessary statically initialized hook.Maxime Dénès
2017-11-19[parser] Remove unnecessary statically initialized hook.Emilio Jesus Gallego Arias
2017-11-19[lib] Minor pending cleanup to consolidate helper function.Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-04[api] Deprecate all legacy uses of Name.Id in core.Emilio Jesus Gallego Arias
2017-10-28Fixing #5401 (printing of patterns with bound anonymous variables).Hugo Herbelin
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
2017-08-29A little reorganization of notations + a fix to #5608.Hugo Herbelin
2017-08-01Detyping functions are now operating on EConstr.t.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-15Merge PR#719: Constrexpr.Numeral without bigintMaxime Dénès
2017-06-14Merge PR#765: Remove obsolete Show commandsMaxime Dénès
2017-06-14[print] Allow Selective Printing of NotationsEmilio Jesus Gallego Arias
2017-06-14Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Pierre Letouzey
2017-06-12Remove more dead code (follow-up of previous commit).Théo Zimmermann
2017-06-08Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-06Merge PR#716: Don't double up on periods in anomaliesMaxime Dénès
2017-06-05Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...Maxime Dénès
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-05-31Using a more explicit algebraic type for evars of kind "MatchingVar".Hugo Herbelin
2017-05-31Creating a module Nameops.Name extending module Names.Name.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 06:17:37 +0000