aboutsummaryrefslogtreecommitdiff
path: root/pretyping/patternops.ml
AgeCommit message (Expand)Author
2019-04-16Clean the representation of recursive annotation in ConstrexprMaxime Dénès
2019-04-10Remove calls to Global.env in PatternopsMaxime Dénès
2019-04-10Remove one call to Global.env in DetypingMaxime Dénès
2019-03-18Fix constr_matching on SPropGaëtan Gilbert
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2018-12-12Merge PR #8974: Fix mod_subst wrt universe polymorphismMaxime Dénès
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-12-05Fix mod_subst wrt universe polymorphismGaëtan Gilbert
2018-10-02Revert #6651: Use r.(p) syntax to print primitive projectionsMaxime Dénès
2018-07-24Projections use index representationGaëtan Gilbert
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-05-25Remove some occurrences of Evd.emptyMaxime Dénès
2018-05-23Moving Option.smart_map to Option.Smart.map.Hugo Herbelin
2018-05-23Collecting List.smart_* functions into a module List.Smart.Hugo Herbelin
2018-05-23Collecting Array.smart_* functions into a module Array.Smart.Hugo Herbelin
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-03-28Supporting fix/cofix in Ltac pattern-matching (wish #7092).Hugo Herbelin
2018-03-28Patterns: Accepting patterns in PFix and PCofix and not only constr.Hugo Herbelin
2018-03-28Patternops: renaming an internal function to more closely match its effect.Hugo Herbelin
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-01-30Use r.(p) syntax to print primitive projections.Maxime Dénès
2017-11-23Make some functions on terms more robust w.r.t new term constructs.Maxime Dénès
2017-11-13[api] Another large deprecation, `Nameops`Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-10-28Fixing #5401 (printing of patterns with bound anonymous variables).Hugo Herbelin
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
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
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-19Fixing an extra bug with pattern_of_constr.Hugo Herbelin
2017-05-17fix swapping of ids in tuples, bug 5486Paul Steckler
2017-05-17Merge branch 'v8.6'Pierre-Marie Pédrot
2017-05-01Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).Hugo Herbelin
2017-04-28Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions with evars)."Maxime Dénès
2017-04-28Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).Hugo Herbelin
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-25[location] [ast] Port module AST to CAstEmilio Jesus Gallego Arias
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:09:11 +0000