aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2009-09-14Backtrack on the forced discharge of type class variables introducedmsozeau
2009-09-14- Addition of "Reserved Infix" continued.herbelin
2009-09-11Generalized the possibility to refer to a global name by a notationherbelin
2009-09-02Postpone checking of Local/Global to allow grammar extensions to use itmsozeau
2009-09-02Stop unnecessary use of lazy values for constraints, simplifyingmsozeau
2009-08-14Ajout de la gestion de Local et Global pour les options (au sens deaspiwack
2009-08-13Death of "survive_module" and "survive_section" (the first one washerbelin
2009-08-11Add support for "Infix ... := constr" instead of just "Infix ... := ref".herbelin
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-08-04- Add more precise error localisation when one of the application failsherbelin
2009-08-03Added "etransitivity".herbelin
2009-08-02Improved parameterization of Coq:herbelin
2009-07-08Use user-given implicits from the arity in inductive definitions.msozeau
2009-07-07Jolification : tentative de supprimer les "( evd)" et associés quiaspiwack
2009-07-01Support for binding Coq root read-only in -R optionherbelin
2009-06-18Use more consistent resolution parameters in Program and regular typingmsozeau
2009-06-18Fix "unsatisfiable constraints" error messages to include all themsozeau
2009-06-13Correct typo: -noglob takes no argument.msozeau
2009-06-11Use a lazy value for the message in FailError, so that it won't bemsozeau
2009-05-27Fix implicit args code so that declarations are added for allmsozeau
2009-05-27Stop using a "Manual Implicit Arguments" flag and support them as soonmsozeau
2009-05-16Minor fixes in typeclasses:msozeau
2009-05-13 Fix to my last notation patch: now fixpoint are correctly handled vsiles
2009-05-09- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceherbelin
2009-04-30Fix a small notation/scope bug:vsiles
2009-04-27- Fixed a little bug in previous commit (bad failure in case of unknown entry).herbelin
2009-04-27- Cleaning (unification of ML names, removal of obsolete code,herbelin
2009-04-25- Fixing #2090 (occur check missing when trying to solve evar-evar equation).herbelin
2009-04-24Backporting 12080 (fixing bug #2091 on bad rollback in the "where"herbelin
2009-04-16Fix bug #2089: correctly dealing with parameters and real arguments inmsozeau
2009-04-08Some dead code removal + cleanupsletouzey
2009-04-08- Fixing bug #2084 (unification not checking sort constraints), hopingherbelin
2009-04-08- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixingherbelin
2009-03-28Rewrite of Program Fixpoint to overcome the previous limitations: msozeau
2009-03-27Remove unused mli filesletouzey
2009-03-22Backport from v8.2 branch of 11986 (interpretation of quantifiedherbelin
2009-03-20Many changes in the Makefile infrastructure + a beginning of ocamlbuildletouzey
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
2009-03-17- configure: affiche si le natdynlink est positionnebarras
2009-03-16Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"herbelin
2009-03-14Better mechanism for loading initial pluginsletouzey
2009-03-09Optionally list opaque constants in addition to axions/variables inmsozeau
2009-03-04Timeout message was not always displayedbarras
2009-03-04commande Timeout + compaction des traces de debug_tacticbarras
2009-03-04Backtrack sur la mémoïsation de nf_evar.aspiwack
2009-02-27=?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...aspiwack
2009-02-19On remplace evar_map par evar_defs (seul evar_defs est désormais exporté aspiwack
2009-02-11Fix de divers petits problèmes d'installationnotin
2009-02-11Report des revisions #11826, #11828 et #11829 de v8.2 vers trunknotin
2009-02-03Allow to turn contrib/subtac into a (nat)dynlink'able pluginletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 01:16:24 +0000