aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation.ml
Commit message (Expand)AuthorAge
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Notation: option to attach extra pretty printing rules to notationsGravatar Enrico Tassi2014-09-29
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Fix HoTT bug #84, binding scopes to projections.Gravatar Matthieu Sozeau2014-06-17
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Fixing generic hashes and replacing them with proper ones.Gravatar Pierre-Marie Pédrot2014-03-03
* Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codeGravatar Pierre Letouzey2014-03-02
* Fixing pervasive comparisonsGravatar Pierre-Marie Pédrot2014-03-01
* Useless check when loading notations through import.Gravatar Pierre-Marie Pédrot2014-03-01
* Reverting the old LIFO behaviour of the notation finding algorithm.Gravatar ppedrot2013-11-08
* Do not generate useless argument arrays in whd_* functions.Gravatar ppedrot2013-10-29
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
* Some more hand-written comparison functions to avoid polymorphic comparison.Gravatar xclerc2013-10-14
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* Actually using the domain function for maps.Gravatar ppedrot2013-08-25
* More dynamic argument scopesGravatar letouzey2013-07-17
* Removing useless uses of Gmap.Gravatar ppedrot2013-05-14
* Getting rid of module Gmapl.Gravatar ppedrot2013-05-09
* Removing Gmap from Notations.Gravatar ppedrot2013-05-09
* Uniformizing the [if_warn] flag used for warning printing and putGravatar ppedrot2013-05-08
* States: frozen states can hold closuresGravatar gareuselesinge2013-05-06
* code simplifications concerning SummaryGravatar letouzey2013-04-22
* Restrict (try...with...) to avoid catching critical exn (part 8)Gravatar letouzey2013-03-13
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Actually adding backtrace handling.Gravatar ppedrot2013-01-28
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Renamed Option.Misc.compare to the more uniform Option.equal.Gravatar ppedrot2012-12-13
* Monomorphization (interp)Gravatar ppedrot2012-11-25
* More equality functionsGravatar ppedrot2012-11-25
* Taking into account the type of a definition (if it exists), and theGravatar herbelin2012-11-17
* Added a CString module.Gravatar ppedrot2012-11-13
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Bigint: avoid dependency over PpGravatar letouzey2012-07-30
* Open Scope can now also accepts delimiters (e.g. Z).Gravatar letouzey2012-07-05
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Internalization of pattern is done in two phases.Gravatar pboutill2012-06-14
* Replacing some str with strbrkGravatar ppedrot2012-06-04
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Stuff about notation_constr (ex-aconstr) now in notation_ops.mlGravatar letouzey2012-05-29
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* Glob_term now mli-only, operations now in Glob_opsGravatar letouzey2012-05-29
* Notations are back in the "in" clause of pattern matching.Gravatar pboutill2012-05-15
* Slight change in the semantics of arguments scopes: scopes can noGravatar herbelin2012-03-26