aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Expand)AuthorAge
* Experiment propagation of implicit arguments and arguments scope forGravatar herbelin2009-11-12
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
* Improving abbreviations/notations + backtrack of semantic change in r12439Gravatar herbelin2009-11-11
* Deactivation of (intrusive) printing of abbreviations from non-imported modules.Gravatar herbelin2009-11-09
* 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
* Misc fixes.Gravatar msozeau2009-11-06
* Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.Gravatar gmelquio2009-11-04
* list, length, app are migrated from List to DatatypesGravatar letouzey2009-11-02
* Revision 12439 continued, printing part (notations to names behaveGravatar herbelin2009-10-29
* Made that notations to names behave like the names they refer to wrtGravatar herbelin2009-10-28
* Fixed a bug when reporting unexisting reference to an inductiveGravatar herbelin2009-10-28
* Add a new vernacular command for controling implicit generalization ofGravatar msozeau2009-10-27
* Local/Global revision 12418 continuedGravatar herbelin2009-10-26
* New cleaning phase of the Local/Global option managementGravatar herbelin2009-10-26
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 16:49:25 +0000