aboutsummaryrefslogtreecommitdiff
path: root/pretyping/glob_ops.ml
AgeCommit message (Expand)Author
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
2017-04-24[location] Switch glob_constr to Loc.locatedEmilio Jesus Gallego Arias
2017-04-24[location] Move Glob_term.predicate_pattern to located.Emilio Jesus Gallego Arias
2017-04-24[location] Move Glob_term.cases_pattern to located.Emilio Jesus Gallego Arias
2017-04-13Using fold_glob_constr_with_binders to code bound_glob_vars.Hugo Herbelin
2017-04-13Adding a fold_glob_constr_with_binders combinator.Hugo Herbelin
2017-04-07Better support for printing constructors with let-ins.Hugo Herbelin
2017-03-24Replacing "cast surgery" in LetIn by a proper field (see PR #404).Hugo Herbelin
2016-07-18A new step on using alpha-conversion in printing notations.Hugo Herbelin
2016-07-17Partial fix to #4592 (notation requiring alpha-conversion for printing).Hugo Herbelin
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-04-19Fixing #4677 (collision of a global variable and of a local variableHugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2015-10-11Fixing untimely unexpected warning "Collision between bound variables" (#4317).Hugo Herbelin
2015-10-11Fixing obviously untested fold_glob_constr and iter_glob_constr.Hugo Herbelin
2015-01-12Update headers.Maxime Dénès
2014-11-19Printing function for [uconstr].Arnaud Spiwack
2014-11-19Glob-ops: a name-mapping operation for pattern-matching binders.Arnaud Spiwack
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
2014-09-17Revert specific syntax for primitive projections, avoiding uglyMatthieu Sozeau
2014-09-12Parsing evar instances.Hugo Herbelin
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-02Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codePierre Letouzey
2014-03-02Adding an equality function over glob_constrPierre-Marie Pédrot
2013-11-27Adding generic solvers to term holes. For now, no resolution mechanism norPierre-Marie Pédrot
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:08:45 +0000