aboutsummaryrefslogtreecommitdiff
path: root/interp/notation.ml
AgeCommit message (Expand)Author
2014-06-17Fix HoTT bug #84, binding scopes to projections.Matthieu Sozeau
2014-06-17Removing dead code.Pierre-Marie Pédrot
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-03Fixing generic hashes and replacing them with proper ones.Pierre-Marie Pédrot
2014-03-02Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codePierre Letouzey
2014-03-01Fixing pervasive comparisonsPierre-Marie Pédrot
2014-03-01Useless check when loading notations through import.Pierre-Marie Pédrot
2013-11-08Reverting the old LIFO behaviour of the notation finding algorithm.ppedrot
2013-10-29Do not generate useless argument arrays in whd_* functions.ppedrot
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-23cList: set-as-list functions are now with an explicit comparisonletouzey
2013-10-14Some more hand-written comparison functions to avoid polymorphic comparison.xclerc
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-08-25Actually using the domain function for maps.ppedrot
2013-07-17More dynamic argument scopesletouzey
2013-05-14Removing useless uses of Gmap.ppedrot
2013-05-09Getting rid of module Gmapl.ppedrot
2013-05-09Removing Gmap from Notations.ppedrot
2013-05-08Uniformizing the [if_warn] flag used for warning printing and putppedrot
2013-05-06States: frozen states can hold closuresgareuselesinge
2013-04-22code simplifications concerning Summaryletouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 8)letouzey
2013-02-19Dir_path --> DirPathletouzey
2013-01-28Actually adding backtrace handling.ppedrot
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-13Renamed Option.Misc.compare to the more uniform Option.equal.ppedrot
2012-11-25Monomorphization (interp)ppedrot
2012-11-25More equality functionsppedrot
2012-11-17Taking into account the type of a definition (if it exists), and theherbelin
2012-11-13Added a CString module.ppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-08Updating headers.herbelin
2012-07-30Bigint: avoid dependency over Ppletouzey
2012-07-05Open Scope can now also accepts delimiters (e.g. Z).letouzey
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-06-04Replacing some str with strbrkppedrot
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
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-05-29Glob_term now mli-only, operations now in Glob_opsletouzey
2012-05-15Notations are back in the "in" clause of pattern matching.pboutill
2012-03-26Slight change in the semantics of arguments scopes: scopes can noherbelin
2012-03-20Continuing r15045-15046 and r15055 (fixing bug #2732 about atomicherbelin
2012-03-02Noise for nothingpboutill
2012-01-05Backtracking on r14876 (fix for bug #2267): extra scopes might beherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 06:14:00 +0000