aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Expand)Author
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
2010-06-09Fix bug #2262: bad implicit argument number by avoiding countingmsozeau
2010-06-08Fixed wrong spelling in a warning.herbelin
2010-06-08Fix treatment of {struct x} annotations in presence of generalizedmsozeau
2010-05-20Fix bug 2307pboutill
2010-05-19Nicer representation of tokens, more independant of camlp*letouzey
2010-04-29Various minor improvements of comments in mli for ocamldocletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Removed obsolete v7->v8 translation code (function check_same_type isherbelin
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2010-04-18Fixed some printing bugs.herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 18:14:44 +0000