aboutsummaryrefslogtreecommitdiff
path: root/interp/constrintern.ml
AgeCommit message (Expand)Author
2012-01-20Added documentation for "Set Parsing Explicit" + fixed mistakenlyherbelin
2012-01-20Added new command "Set Parsing Explicit" for deactivating parsing (andherbelin
2012-01-19Boolean Option Patterns Compatibilitypboutill
2012-01-16Parameters in pattern first step.pboutill
2012-01-05Backtracking on r14876 (fix for bug #2267): extra scopes might beherbelin
2012-01-04Fixing Arguments Scope bug when too many scopes are given (bug #2667).herbelin
2011-12-17A pass on warning printings. Made systematic the use of msg_warning soherbelin
2011-11-16Fixing association of wrong "as"-pattern name when expandingherbelin
2011-10-28Remove dynamic stuff from constr_expr and glob_constrglondu
2011-07-22Add a syntax entry for fully applied constructor patternpboutill
2011-07-22Internalization of pattern carries a full intern_envpboutill
2011-07-15A correct error message for an unknown field in a record definitionpboutill
2011-05-26Partial fix for accepting bound variables with same name as implicitherbelin
2011-04-25Fixing and completing interpretation of let's in notations for iterated binders.herbelin
2011-04-13- Remove create_evar_defsmsozeau
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
2010-12-25Rename mkR* smart constructors (mostly in funind)glondu
2010-12-24More {raw => glob} changes for consistencyglondu
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
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-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-13Fix unescaped end-of-lines (OCaml warning 29)glondu
2010-09-10Bugfix: A notation for a constructor where some arguments are _pboutill
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-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-08Fix treatment of {struct x} annotations in presence of generalizedmsozeau
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-10Partially fixed bug #2231 (an inductive parameter name was internallyherbelin
2010-04-05Improving compatibility between 8.2 and 8.3herbelin
2010-03-29Several bug-fixes and improvements of coqdocherbelin
2010-01-28Backport fixes in Instance declarations to Program Instance.msozeau
2009-12-24In "simpl c" and "change c with d", c can be a pattern.herbelin
2009-11-27Added support for definition of fixpoints using tactics.herbelin
2009-11-12Experiment propagation of implicit arguments and arguments scope forherbelin
2009-11-11Improving abbreviations/notations + backtrack of semantic change in r12439herbelin
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 04:50:58 +0000