aboutsummaryrefslogtreecommitdiff
path: root/interp/notation_ops.ml
AgeCommit message (Expand)Author
2015-03-24Fixing equality of notation_constrs. Fixes bug #4136.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
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-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-09-08Parsing of Type@{max(i,j)}.Matthieu Sozeau
2014-05-06Fix inversion of notations for projections.Matthieu Sozeau
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-02Removing generic equality in Syntax plugin.Pierre-Marie Pédrot
2014-03-02Adding an equality function over glob_constrPierre-Marie Pédrot
2014-03-01Fixing pervasive comparisonsPierre-Marie Pédrot
2013-12-22Notations now accept the $(...)$ tactic-in-term syntax. They are resolved atPierre-Marie Pédrot
2013-12-22Notations can now accept dummy arguments. If ever a bound variable is notPierre-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-10-24Restore my version of notation_ops.ml now that List.remove_assoc_f is fixedletouzey
2013-10-24Oups, repair the compilation (micromega + Morphism_prop)letouzey
2013-10-24Turn many List.assoc into List.assoc_fletouzey
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-08-03Replacing uses of association lists by maps in notations.ppedrot
2013-05-05Relaxing the constraint on eta-expanding on the fly while looking forherbelin
2013-01-07Fixup notation printing in patternspboutill
2012-12-18Modulification of nameppedrot
2012-12-14Modulification of identifierppedrot
2012-11-25Monomorphization (interp)ppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-09-15Some documentation and cleaning of CList and Util interfaces.ppedrot
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-08Updating headers.herbelin
2012-07-20Fixup implicits in patterns & notationspboutill
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-14Constrextern is allow to use partially applied notationspboutill
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29Stuff about notation_constr (ex-aconstr) now in notation_ops.mlletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:32:48 +0000