aboutsummaryrefslogtreecommitdiff
path: root/interp/constrexpr_ops.ml
AgeCommit message (Expand)Author
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
2013-11-27Adding generic solvers to term holes. For now, no resolution mechanism norPierre-Marie Pédrot
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2012-12-18Modulification of nameppedrot
2012-12-18Fixing parsing of specific primitive tokens used as notations for patternsherbelin
2012-12-14Modulification of identifierppedrot
2012-12-14Implemented a full-fledged equality on [constr_expr]. By the way,ppedrot
2012-11-25More equality functionsppedrot
2012-11-13More monomorphizationsppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-14Internalization of pattern is done in two phases.pboutill
2012-05-29Basic stuff about constr_expr migrated from topconstr to constrexpr_opsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 19:21:23 +0000