aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.ml
Commit message (Expand)AuthorAge
* 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
* Rename mkR* smart constructors (mostly in funind)Gravatar glondu2010-12-25
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* 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
* 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 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
* 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
* 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
* Fix bug #2262: bad implicit argument number by avoiding countingGravatar msozeau2010-06-09
* Fix treatment of {struct x} annotations in presence of generalizedGravatar msozeau2010-06-08
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Partially fixed bug #2231 (an inductive parameter name was internallyGravatar herbelin2010-04-10
* Improving compatibility between 8.2 and 8.3Gravatar herbelin2010-04-05
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
* Backport fixes in Instance declarations to Program Instance.Gravatar msozeau2010-01-28
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
* Experiment propagation of implicit arguments and arguments scope forGravatar herbelin2009-11-12
* Improving abbreviations/notations + backtrack of semantic change in r12439Gravatar herbelin2009-11-11
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Use generalizable variables info when internalizing arbitrary bindings,Gravatar msozeau2009-11-08
* Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.Gravatar gmelquio2009-11-04
* Made that notations to names behave like the names they refer to wrtGravatar herbelin2009-10-28
* Fixed a notation bug when extending binder_constr with empty levelsGravatar herbelin2009-10-17
* Fix bug #2162 and a name clashing bug in generalized binders.Gravatar msozeau2009-10-09
* Fixed error message "cannot infer the type of id" in presence ofGravatar herbelin2009-09-27
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Jolification : tentative de supprimer les "( evd)" et associés quiGravatar aspiwack2009-07-07
* Fixes for r12197, the refined evars were not returned in case fail_evarGravatar msozeau2009-06-22
* Use more consistent resolution parameters in Program and regular typingGravatar msozeau2009-06-18
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 18:50:01 +0000