aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Expand)Author
2009-03-28Rewrite of Program Fixpoint to overcome the previous limitations: msozeau
2009-03-20Many changes in the Makefile infrastructure + a beginning of ocamlbuildletouzey
2009-02-19On remplace evar_map par evar_defs (seul evar_defs est désormais exporté aspiwack
2009-02-06pushed evar reduction in kernelbarras
2009-02-06Fixing #2044 (bad printing of primitive notation at the head ofherbelin
2009-01-20Fixing a bug in 11804 (support for _ in ident entry of notations). herbelin
2009-01-19- Structuring Numbers and fixing Setoid in stdlib's doc.herbelin
2009-01-17DISCLAIMERpuech
2009-01-01Switched to "standardized" names for the properties of eq andherbelin
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-22Fix bugs #1975 and #1976.msozeau
2008-10-22A much better implementation of implicit generalization:msozeau
2008-10-22Affichage des notations récursives:herbelin
2008-10-19- Export de pattern_ident vers les ARGUMENT EXTEND and co.herbelin
2008-10-14Dumpglob.dump_modref : fix an assert failureletouzey
2008-10-11Backporting 11445 from 8.2 to trunk (negative conditions inherbelin
2008-10-08Améliorations de l'affichage des coercions suggérées par Georges :herbelin
2008-09-15Fix bug #1943 and restrict the inference optimisation of Program tomsozeau
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-08-04Évolutions diverses et variées.herbelin
2008-07-24Suite commit 11236notin
2008-07-23Stop glob messages to be printed by default on stdout letouzey
2008-07-22Correct implementation of discharging of implicit arguments and add newmsozeau
2008-07-22Oubli lors du commit #11236notin
2008-07-21Suite commit 11236notin
2008-07-18Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...notin
2008-07-18Modification rapide du message d'erreur lorsqu'un _ ne peut êtreherbelin
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-07- Improve [Context] vernacular to allow arbitrary binders, not justmsozeau
2008-07-04Fixes in handling of implicit arguments:msozeau
2008-07-01Documentation Prop<=Set et Arguments Scope Globalherbelin
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
2008-06-14Correction bug 1878 (utilisation de extend_evar déplacée là où uneherbelin
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
2008-06-06Enhancements to coqdoc, better globalization of sections and modules.msozeau
2008-06-03Fix setoid_rewrite documentation examples.msozeau
2008-05-30Improvements on coqdoc by adding more information into .globmsozeau
2008-05-28Notation concise pour la valeur par défaut des cas reconnus commeherbelin
2008-05-24Ajout de la possibilité d'utiliser fix/cofix dans les notations.herbelin
2008-05-12Fix "not an applied typeclass" error for legitimate classesmsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 18:40:02 +0000