aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Expand)AuthorAge
* Fixed some printing bugs.Gravatar herbelin2010-04-18
* Optimized need for delimiters when disjoint scopes for strings andGravatar herbelin2010-04-10
* Partially fixed bug #2231 (an inductive parameter name was internallyGravatar herbelin2010-04-10
* Improving compatibility between 8.2 and 8.3Gravatar herbelin2010-04-05
* Small things about coqdoc + fixing lettuple.v test (part of bug #2289)Gravatar herbelin2010-03-30
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
* Fix implicit_application for let-bound variables in the class context.Gravatar msozeau2010-01-28
* Backport fixes in Instance declarations to Program Instance.Gravatar msozeau2010-01-28
* Variant !F M for functor application that does not honor the Inline declarationsGravatar letouzey2010-01-17
* Include can accept both Module and Module TypeGravatar letouzey2010-01-07
* Allowed handling of partly-applied record constructors. (Fix for bug #2196.)Gravatar gmelquio2010-01-06
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
* Opened the possibility to type Ltac patterns but it is not fully functional yetGravatar herbelin2009-12-24
* Generic support for open terms in tacticsGravatar herbelin2009-12-21
* Made the interpretation levels rlevel/glevel/tlevel truly phantomGravatar herbelin2009-12-19
* Deactivating printing of {| |} for records when option Printing All is set.Gravatar herbelin2009-12-13
* Fixed incorrect computation of possible guard in presence of `{ ... } contexts.Gravatar herbelin2009-12-12
* No more specific syntax "Include Self" for inclusion of partially-applied fun...Gravatar letouzey2009-12-07
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
* Module subtyping : allow many <: and module type declaration with <:Gravatar letouzey2009-11-18
* New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))Gravatar letouzey2009-11-16
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-09 08:10:19 +0000