aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* 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
* Fix a small notation/scope bug:Gravatar vsiles2009-04-30
* - Fixed a little bug in previous commit (bad failure in case of unknown entry).Gravatar herbelin2009-04-27
* - Cleaning (unification of ML names, removal of obsolete code,Gravatar herbelin2009-04-27
* - Fixing #2090 (occur check missing when trying to solve evar-evar equation).Gravatar herbelin2009-04-25
* Backporting 12080 (fixing bug #2091 on bad rollback in the "where"Gravatar herbelin2009-04-24
* Fix bug #2089: correctly dealing with parameters and real arguments inGravatar msozeau2009-04-16
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* - Fixing bug #2084 (unification not checking sort constraints), hopingGravatar herbelin2009-04-08
* - Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixingGravatar herbelin2009-04-08
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* Remove unused mli filesGravatar letouzey2009-03-27
* Backport from v8.2 branch of 11986 (interpretation of quantifiedGravatar herbelin2009-03-22
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20
* - configure: affiche si le natdynlink est positionneGravatar barras2009-03-17
* Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"Gravatar herbelin2009-03-16
* Better mechanism for loading initial pluginsGravatar letouzey2009-03-14
* Optionally list opaque constants in addition to axions/variables inGravatar msozeau2009-03-09
* Timeout message was not always displayedGravatar barras2009-03-04
* commande Timeout + compaction des traces de debug_tacticGravatar barras2009-03-04
* Backtrack sur la mémoïsation de nf_evar.Gravatar aspiwack2009-03-04
* =?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...Gravatar aspiwack2009-02-27
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* Fix de divers petits problèmes d'installationGravatar notin2009-02-11
* Report des revisions #11826, #11828 et #11829 de v8.2 vers trunkGravatar notin2009-02-11
* Allow to turn contrib/subtac into a (nat)dynlink'able pluginGravatar letouzey2009-02-03
* Revert changes in pcoq functions to restore compatibility with contribsGravatar puech2009-01-26
* Petit nettoyage faisant suite au commit #11847 .Gravatar aspiwack2009-01-23
* Les records déclarés avec Record ne peuvent plus être récursifs (le Gravatar aspiwack2009-01-19
* - Structuring Numbers and fixing Setoid in stdlib's doc.Gravatar herbelin2009-01-19
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
* Getting rid of the previous implementation of setoid_rewrite which wasGravatar msozeau2009-01-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 05:27:04 +0000