aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Expand)AuthorAge
* Remove useless Liboject.export_function fieldGravatar glondu2009-09-17
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Added "etransitivity".Gravatar herbelin2009-08-03
* 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
* - Added two new introduction patterns with the following temptative syntaxes:Gravatar herbelin2009-06-07
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
* Fix a small notation/scope bug:Gravatar vsiles2009-04-30
* - Cleaning (unification of ML names, removal of obsolete code,Gravatar herbelin2009-04-27
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* pushed evar reduction in kernelGravatar barras2009-02-06
* Fixing #2044 (bad printing of primitive notation at the head ofGravatar herbelin2009-02-06
* 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
* DISCLAIMERGravatar puech2009-01-17
* Switched to "standardized" names for the properties of eq andGravatar herbelin2009-01-01
* - 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
* Fix bugs #1975 and #1976.Gravatar msozeau2008-10-22
* A much better implementation of implicit generalization:Gravatar msozeau2008-10-22
* Affichage des notations récursives:Gravatar herbelin2008-10-22
* - Export de pattern_ident vers les ARGUMENT EXTEND and co.Gravatar herbelin2008-10-19
* Dumpglob.dump_modref : fix an assert failureGravatar letouzey2008-10-14
* Backporting 11445 from 8.2 to trunk (negative conditions inGravatar herbelin2008-10-11
* Améliorations de l'affichage des coercions suggérées par Georges :Gravatar herbelin2008-10-08
* Fix bug #1943 and restrict the inference optimisation of Program toGravatar msozeau2008-09-15
* 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
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Suite commit 11236Gravatar notin2008-07-24
* Stop glob messages to be printed by default on stdout Gravatar letouzey2008-07-23
* Correct implementation of discharging of implicit arguments and add newGravatar msozeau2008-07-22
* Oubli lors du commit #11236Gravatar notin2008-07-22
* Suite commit 11236Gravatar notin2008-07-21
* Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...Gravatar notin2008-07-18
* Modification rapide du message d'erreur lorsqu'un _ ne peut êtreGravatar herbelin2008-07-18
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Autour du parsing:Gravatar herbelin2008-07-15