aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Expand)AuthorAge
* Definitions of positive, N, Z moved in Numbers/BinNums.vGravatar letouzey2011-05-05
* Fixing and completing interpretation of let's in notations for iterated binders.Gravatar herbelin2011-04-25
* Yet another bug in printing fix with let-in bindersGravatar herbelin2011-04-24
* Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".Gravatar herbelin2011-04-15
* - Remove create_evar_defsGravatar msozeau2011-04-13
* Fixing multiple printing bugs with "Notation f x := ..."Gravatar herbelin2011-04-08
* Did that adding a rule for printing applications as "f(x)" works.Gravatar herbelin2011-03-31
* Added a table for using reserved names for binding names to typesGravatar herbelin2011-03-05
* Moving printing of module typing errors upwards to himsg.ml so as toGravatar herbelin2011-03-05
* fix last commit about modules (subst_cl_typ may raise Not_found)Gravatar letouzey2011-02-12
* An automatic substitution of scope at functor applicationGravatar letouzey2011-02-11
* Annotations at functor applications:Gravatar letouzey2011-02-11
* Fixpoints are traverse during implicits arguments search to toplevelGravatar pboutill2011-02-10
* Interp a definition with the implicit arguments of its local contextGravatar pboutill2011-02-10
* local variables can have implicits locallyGravatar pboutill2011-02-10
* Data structure telling implicits of local variables is a map in theGravatar pboutill2011-02-10
* internalize now use a record for its envGravatar pboutill2011-02-10
* More comments and less doublons in some mliGravatar pboutill2011-02-10
* Coqlib.gen_constant_in_modules can take a qualid string "Foo.bar"Gravatar letouzey2011-01-31
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* Rename mkR* smart constructors (mostly in funind)Gravatar glondu2010-12-25
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
* Fix diagram in genarg.mliGravatar glondu2010-12-23
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Prepare change of nomenclature rawconstr -> glob_constrGravatar glondu2010-12-23
* Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).Gravatar herbelin2010-12-04
* Fixing several bugs with links to notation in coqdoc, including bug #2445:Gravatar herbelin2010-12-04
* Add information of localisation when an error involving an "implicitGravatar herbelin2010-11-07
* Fixing a regression wrt 8.2 when using an "ident" several times in a notationGravatar herbelin2010-11-04
* Move stuff about positive into a distinct PArith subdirGravatar letouzey2010-11-02
* Cleaning the use of parentheses around evd and evdref (cosmetic commit).Gravatar herbelin2010-10-31
* Added multiple implicit arguments rules per name.Gravatar herbelin2010-10-03
* Fix function applications without labels (OCaml warning 6)Gravatar glondu2010-09-28
* Partial review of removed dead code (r13460)Gravatar herbelin2010-09-24
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Fix unescaped end-of-lines (OCaml warning 29)Gravatar glondu2010-09-13
* Bugfix: A notation for a constructor where some arguments are _Gravatar pboutill2010-09-10
* Fixed a bug introduced (r13316/r13329) in the printing of notationsGravatar herbelin2010-07-29
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
* Simplified the way internalization_data (i.e. bindings of bound varsGravatar herbelin2010-07-22
* Constrintern: unified push_name_env and push_loc_name_env; madeGravatar herbelin2010-07-22
* Constrintern: Moved section about binders before section about notationGravatar herbelin2010-07-22
* Switch to American spelling for "internalise" and "internalisation"Gravatar herbelin2010-07-22
* Move [delayed] to util and use [force_delayed] everywhere to forceGravatar msozeau2010-06-30
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Added printing of recursive notations in cases pattern (supported by wish 2248).Gravatar herbelin2010-06-14
* Fixing bug 2295 (omission of option "as" in return clause of "match" was notGravatar herbelin2010-06-13
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12