aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Expand)Author
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
2010-04-10Optimized need for delimiters when disjoint scopes for strings andherbelin
2010-04-10Partially fixed bug #2231 (an inductive parameter name was internallyherbelin
2010-04-05Improving compatibility between 8.2 and 8.3herbelin
2010-03-30Small things about coqdoc + fixing lettuple.v test (part of bug #2289)herbelin
2010-03-29Several bug-fixes and improvements of coqdocherbelin
2010-01-28Fix implicit_application for let-bound variables in the class context.msozeau
2010-01-28Backport fixes in Instance declarations to Program Instance.msozeau
2010-01-17Variant !F M for functor application that does not honor the Inline declarationsletouzey
2010-01-07Include can accept both Module and Module Typeletouzey
2010-01-06Allowed handling of partly-applied record constructors. (Fix for bug #2196.)gmelquio
2009-12-24In "simpl c" and "change c with d", c can be a pattern.herbelin
2009-12-24Opened the possibility to type Ltac patterns but it is not fully functional yetherbelin
2009-12-21Generic support for open terms in tacticsherbelin
2009-12-19Made the interpretation levels rlevel/glevel/tlevel truly phantomherbelin
2009-12-13Deactivating printing of {| |} for records when option Printing All is set.herbelin
2009-12-12Fixed incorrect computation of possible guard in presence of `{ ... } contexts.herbelin
2009-12-07No more specific syntax "Include Self" for inclusion of partially-applied fun...letouzey
2009-11-27Added support for definition of fixpoints using tactics.herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 08:24:29 +0000