aboutsummaryrefslogtreecommitdiff
path: root/pretyping/glob_ops.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 InductiveopsMaxime Dénès
2019-04-10Remove calls to Global.env in Glob_opsMaxime Dénès
2019-03-18Fix constr_matching on SPropGaëtan Gilbert
2019-02-28Constructor type information uses the expanded form.Pierre-Marie Pédrot
2019-02-19Notations: Enforce strong evaluation of cases_pattern_of_glob_constr.Hugo Herbelin
2019-02-04Primitive integersMaxime Dénès
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-10-02Revert #6651: Use r.(p) syntax to print primitive projectionsMaxime Dénès
2018-09-10Moving part of pretyping dealing with ltac and renaming in new module GlobEnv.Hugo Herbelin
2018-07-17change into QuestionMark defaultSiddharth Bhat
2018-07-17Change QuestionMark for better record field missing error message.Siddharth Bhat
2018-07-03Glob_ops.rename_glob_vars: fix typoGaëtan Gilbert
2018-07-03Glob_ops.fix_kind_eq: fix typoGaëtan Gilbert
2018-06-18Remove reference name type.Maxime Dénès
2018-06-17Fixes #7811 (uncaught Not_found in notation printer related to "match").Hugo Herbelin
2018-06-14Merge PR #7105: Getting rid of some false "collision between bound variable n...Matthieu Sozeau
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-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-03-28Glob_ops: cosmetic renaming to reflect the type of objects.Hugo Herbelin
2018-03-28Getting rid of some false "collision between bound variable names" warnings.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-02-20Using an "as" clause when needed for printing irrefutable patterns.Hugo Herbelin
2018-02-20Adding patterns in the category of binders for notations.Hugo Herbelin
2018-02-20Canonically add an encoding in glob_constr of "as" operator for cases_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-11-13[api] Another large deprecation, `Nameops`Emilio Jesus Gallego Arias
2017-10-25[general] Remove Econstr dependency from `intf`Emilio Jesus Gallego Arias
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
2017-09-23Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).Hugo Herbelin
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-09A fix to #5414 (ident bound by ltac names now known for "match").Hugo Herbelin
2017-06-08Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-05Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...Maxime Dénès
2017-06-01Merge PR#561: Improving the Name APIMaxime Dénès
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-31Fixing #5523 (missing support for complex constructions in recursive notations).Hugo Herbelin
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-05Remove dead code and unused open.Maxime Dénès
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
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 00:04:35 +0000