aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Expand)Author
2011-05-05Definitions of positive, N, Z moved in Numbers/BinNums.vletouzey
2011-04-25Fixing and completing interpretation of let's in notations for iterated binders.herbelin
2011-04-24Yet another bug in printing fix with let-in bindersherbelin
2011-04-15Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".herbelin
2011-04-13- Remove create_evar_defsmsozeau
2011-04-08Fixing multiple printing bugs with "Notation f x := ..."herbelin
2011-03-31Did that adding a rule for printing applications as "f(x)" works.herbelin
2011-03-05Added a table for using reserved names for binding names to typesherbelin
2011-03-05Moving printing of module typing errors upwards to himsg.ml so as toherbelin
2011-02-12fix last commit about modules (subst_cl_typ may raise Not_found)letouzey
2011-02-11An automatic substitution of scope at functor applicationletouzey
2011-02-11Annotations at functor applications:letouzey
2011-02-10Fixpoints are traverse during implicits arguments search to toplevelpboutill
2011-02-10Interp a definition with the implicit arguments of its local contextpboutill
2011-02-10local variables can have implicits locallypboutill
2011-02-10Data structure telling implicits of local variables is a map in thepboutill
2011-02-10internalize now use a record for its envpboutill
2011-02-10More comments and less doublons in some mlipboutill
2011-01-31Coqlib.gen_constant_in_modules can take a qualid string "Foo.bar"letouzey
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
2010-12-25Rename mkR* smart constructors (mostly in funind)glondu
2010-12-24More {raw => glob} changes for consistencyglondu
2010-12-23Fix diagram in genarg.mliglondu
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
2010-12-23Prepare change of nomenclature rawconstr -> glob_constrglondu
2010-12-04Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).herbelin
2010-12-04Fixing several bugs with links to notation in coqdoc, including bug #2445:herbelin
2010-11-07Add information of localisation when an error involving an "implicitherbelin
2010-11-04Fixing a regression wrt 8.2 when using an "ident" several times in a notationherbelin
2010-11-02Move stuff about positive into a distinct PArith subdirletouzey
2010-10-31Cleaning the use of parentheses around evd and evdref (cosmetic commit).herbelin
2010-10-03Added multiple implicit arguments rules per name.herbelin
2010-09-28Fix function applications without labels (OCaml warning 6)glondu
2010-09-24Partial review of removed dead code (r13460)herbelin
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-09-13Fix unescaped end-of-lines (OCaml warning 29)glondu
2010-09-10Bugfix: A notation for a constructor where some arguments are _pboutill
2010-07-29Fixed a bug introduced (r13316/r13329) in the printing of notationsherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-22Extension of the recursive notations mechanismherbelin
2010-07-22Simplified the way internalization_data (i.e. bindings of bound varsherbelin
2010-07-22Constrintern: unified push_name_env and push_loc_name_env; madeherbelin
2010-07-22Constrintern: Moved section about binders before section about notationherbelin
2010-07-22Switch to American spelling for "internalise" and "internalisation"herbelin
2010-06-30Move [delayed] to util and use [force_delayed] everywhere to forcemsozeau
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-06-14Added printing of recursive notations in cases pattern (supported by wish 2248).herbelin
2010-06-13Fixing bug 2295 (omission of option "as" in return clause of "match" was notherbelin
2010-06-12Fixing spelling: pr_coma -> pr_commaherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-21 22:56:13 +0000