aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.Gravatar gmelquio2009-11-04
* Hopefully improved layout of fix guardness error message.Gravatar herbelin2009-10-29
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Add a new vernacular command for controling implicit generalization ofGravatar msozeau2009-10-27
* Documentation of the Local and Global modifiers.Gravatar herbelin2009-10-27
* 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
* note for later : when the tag table is shared, never, ever create twoGravatar vgross2009-10-16
* MSets: a new generation of FSetsGravatar letouzey2009-10-13
* Fix bug #2162 and a name clashing bug in generalized binders.Gravatar msozeau2009-10-09
* Correctly do backtracking during type class resolution even if only newGravatar msozeau2009-10-05
* Revert "kills the old backtracking framework and replaces it with"Gravatar vgross2009-10-05
* Changed the way to support compatibility with previous versions.Gravatar herbelin2009-10-04
* Removal of trailing spaces.Gravatar serpyc2009-10-04
* Added option "Unset Dependent Propositions Elimination" to protectGravatar herbelin2009-10-03
* Add support for Local Declare ML ModuleGravatar glondu2009-09-29
* Remove legacy export_* functionsGravatar glondu2009-09-29
* kills the old backtracking framework and replaces it withGravatar vgross2009-09-29
* Fixed a hole in glob_tactic that allowed some Ltac code to refer toGravatar herbelin2009-09-26
* Add the option to automatically introduce variables declared before theGravatar msozeau2009-09-22
* Replace call to where_in_path by find_file_in_path in "Locate File"Gravatar glondu2009-09-17
* Replace unprotected call to where_in_path by find_file_in_pathGravatar glondu2009-09-17
* Remove useless Liboject.export_function fieldGravatar glondu2009-09-17
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Fixed compilation error message which was no longer emacs-compliant sinceGravatar herbelin2009-09-15
* Backtrack on the forced discharge of type class variables introducedGravatar msozeau2009-09-14
* - Addition of "Reserved Infix" continued.Gravatar herbelin2009-09-14
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
* Postpone checking of Local/Global to allow grammar extensions to use itGravatar msozeau2009-09-02
* Stop unnecessary use of lazy values for constraints, simplifyingGravatar msozeau2009-09-02
* Ajout de la gestion de Local et Global pour les options (au sens deGravatar aspiwack2009-08-14
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* Add support for "Infix ... := constr" instead of just "Infix ... := ref".Gravatar herbelin2009-08-11
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* - Add more precise error localisation when one of the application failsGravatar herbelin2009-08-04
* Added "etransitivity".Gravatar herbelin2009-08-03
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
* Use user-given implicits from the arity in inductive definitions.Gravatar msozeau2009-07-08
* Jolification : tentative de supprimer les "( evd)" et associés quiGravatar aspiwack2009-07-07
* Support for binding Coq root read-only in -R optionGravatar herbelin2009-07-01
* Use more consistent resolution parameters in Program and regular typingGravatar msozeau2009-06-18
* Fix "unsatisfiable constraints" error messages to include all theGravatar msozeau2009-06-18
* Correct typo: -noglob takes no argument.Gravatar msozeau2009-06-13
* Use a lazy value for the message in FailError, so that it won't beGravatar msozeau2009-06-11
* Fix implicit args code so that declarations are added for allGravatar msozeau2009-05-27
* Stop using a "Manual Implicit Arguments" flag and support them as soonGravatar msozeau2009-05-27
* Minor fixes in typeclasses:Gravatar msozeau2009-05-16
* Fix to my last notation patch: now fixpoint are correctly handled Gravatar vsiles2009-05-13
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 03:14:14 +0000