aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/topconstr.ml
Commit message (Expand)AuthorAge
...
* Add a syntax entry for fully applied constructor patternGravatar pboutill2011-07-22
* Rather quick hack to avoid using notations involving "Type" whenGravatar herbelin2011-06-12
* Make Notation works with anonymous-level "Type".Gravatar herbelin2011-06-08
* Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".Gravatar herbelin2011-04-15
* Annotations at functor applications:Gravatar letouzey2011-02-11
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* 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
* Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).Gravatar herbelin2010-12-04
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Fixed a bug introduced (r13316/r13329) in the printing of notationsGravatar herbelin2010-07-29
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
* Constrintern: unified push_name_env and push_loc_name_env; madeGravatar herbelin2010-07-22
* Added printing of recursive notations in cases pattern (supported by wish 2248).Gravatar herbelin2010-06-14
* Fix treatment of {struct x} annotations in presence of generalizedGravatar msozeau2010-06-08
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
* Variant !F M for functor application that does not honor the Inline declarationsGravatar letouzey2010-01-17
* Include can accept both Module and Module TypeGravatar letouzey2010-01-07
* Opened the possibility to type Ltac patterns but it is not fully functional yetGravatar herbelin2009-12-24
* Fixed incorrect computation of possible guard in presence of `{ ... } contexts.Gravatar herbelin2009-12-12
* No more specific syntax "Include Self" for inclusion of partially-applied fun...Gravatar letouzey2009-12-07
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
* Module subtyping : allow many <: and module type declaration with <:Gravatar letouzey2009-11-18
* New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))Gravatar letouzey2009-11-16
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.Gravatar gmelquio2009-11-04
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* 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
* - Cleaning (unification of ML names, removal of obsolete code,Gravatar herbelin2009-04-27
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* Fixing a bug in 11804 (support for _ in ident entry of notations). Gravatar herbelin2009-01-20
* - Structuring Numbers and fixing Setoid in stdlib's doc.Gravatar herbelin2009-01-19
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
* Open notation for declaring record instances.Gravatar msozeau2008-10-23
* Generalized implementation of generalization.Gravatar msozeau2008-10-23
* A much better implementation of implicit generalization:Gravatar msozeau2008-10-22
* Affichage des notations récursives:Gravatar herbelin2008-10-22
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Utilisation de try_locate_qualified_library au lieu de locate_qualified_libra...Gravatar notin2008-07-07
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
* Improvements on coqdoc by adding more information into .globGravatar msozeau2008-05-30
* Ajout de la possibilité d'utiliser fix/cofix dans les notations.Gravatar herbelin2008-05-24
* - Prise en compte de l'unicode dans la fonction hdchar (elle fournissait desGravatar herbelin2008-05-10
* Postpone the search for the recursive argument index from the user givenGravatar msozeau2008-05-06
* Ajout d'abbréviations/notations paramétriquesGravatar herbelin2008-03-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 12:36:22 +0000