aboutsummaryrefslogtreecommitdiff
path: root/interp/constrintern.ml
AgeCommit message (Expand)Author
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
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-11-08Use generalizable variables info when internalizing arbitrary bindings,msozeau
2009-11-04Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.gmelquio
2009-10-28Made that notations to names behave like the names they refer to wrtherbelin
2009-10-17Fixed a notation bug when extending binder_constr with empty levelsherbelin
2009-10-09Fix bug #2162 and a name clashing bug in generalized binders.msozeau
2009-09-27Fixed error message "cannot infer the type of id" in presence ofherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-07-07Jolification : tentative de supprimer les "( evd)" et associés quiaspiwack
2009-06-22Fixes for r12197, the refined evars were not returned in case fail_evarmsozeau
2009-06-18Use more consistent resolution parameters in Program and regular typingmsozeau
2009-04-08Some dead code removal + cleanupsletouzey
2009-03-28Rewrite of Program Fixpoint to overcome the previous limitations: msozeau
2009-02-19On remplace evar_map par evar_defs (seul evar_defs est désormais exporté aspiwack
2009-01-19- Structuring Numbers and fixing Setoid in stdlib's doc.herbelin
2009-01-17DISCLAIMERpuech
2008-12-29- Added support for subterm matching in SearchAbout.herbelin
2008-12-14Generalized binding syntax overhaul: only two new binders: `() and `{},msozeau
2008-11-09More factorization of inductive/record and typeclasses: move classmsozeau
2008-11-05Move Record desugaring to constrintern and add ability to use notationsmsozeau
2008-10-26Correct enormous bug in interpretation of generalized binders: it simplymsozeau
2008-10-23Open notation for declaring record instances.msozeau
2008-10-23Generalized implementation of generalization.msozeau
2008-10-22A much better implementation of implicit generalization:msozeau
2008-10-22Affichage des notations récursives:herbelin
2008-09-11Add enough information to correctly globalize recursive calls in inductive andmsozeau
2008-09-07Better handling of the opacity of proof obligations, add the possibility ofmsozeau
2008-07-24Suite commit 11236notin
2008-07-18Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...notin
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-07-15Autour du parsing:herbelin
2008-07-07Utilisation de try_locate_qualified_library au lieu de locate_qualified_libra...notin
2008-07-04Fixes in handling of implicit arguments:msozeau
2008-06-25Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...notin
2008-06-21Code cleanup in typeclasses, remove dead and duplicated code.msozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 01:13:44 +0000