aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.ml
Commit message (Expand)AuthorAge
* 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
* - Structuring Numbers and fixing Setoid in stdlib's doc.Gravatar herbelin2009-01-19
* DISCLAIMERGravatar puech2009-01-17
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* Generalized binding syntax overhaul: only two new binders: `() and `{},Gravatar msozeau2008-12-14
* More factorization of inductive/record and typeclasses: move classGravatar msozeau2008-11-09
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
* Correct enormous bug in interpretation of generalized binders: it simplyGravatar msozeau2008-10-26
* 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
* Add enough information to correctly globalize recursive calls in inductive andGravatar msozeau2008-09-11
* Better handling of the opacity of proof obligations, add the possibility ofGravatar msozeau2008-09-07
* Suite commit 11236Gravatar notin2008-07-24
* Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...Gravatar notin2008-07-18
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Autour du parsing:Gravatar herbelin2008-07-15
* 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
* Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...Gravatar notin2008-06-25
* Code cleanup in typeclasses, remove dead and duplicated code.Gravatar msozeau2008-06-21
* Enhancements to coqdoc, better globalization of sections and modules.Gravatar msozeau2008-06-06
* Fix setoid_rewrite documentation examples.Gravatar msozeau2008-06-03
* Improvements on coqdoc by adding more information into .globGravatar msozeau2008-05-30
* Postpone the search for the recursive argument index from the user givenGravatar msozeau2008-05-06
* Factorize code for internalization of binders to fix bug #1846. AlsoGravatar msozeau2008-05-04
* Correction bug List.map2 dans Case12.vGravatar herbelin2008-04-09
* Modifications diverses et variées :Gravatar herbelin2008-03-30
* Ajout d'abbréviations/notations paramétriquesGravatar herbelin2008-03-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 06:29:38 +0000