aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2008-10-11Backporting 11445 from 8.2 to trunk (negative conditions inherbelin
2008-10-09* Fixed constr_cmp again to handle universes subtyping correctlypuech
2008-10-08Fix bug #1959 (remember: never use a partial functions mindlessly).msozeau
2008-10-08Améliorations de l'affichage des coercions suggérées par Georges :herbelin
2008-10-07fixing r11433 again:barras
2008-10-07fixed pb with r11433barras
2008-10-06bug #1951: polymorphic indtypes: universe subst was not performed in the type...barras
2008-10-06## Lines starting with '## ' will be removed from the log message.msozeau
2008-10-03(Try to) use the conversion oracle also in w_unify to choose which constant tomsozeau
2008-10-03Minor fixes related to coqdoc and --interpolate and the dependentmsozeau
2008-10-02Fixing constr_cmp, propagating subtyping only right of a productpuech
2008-09-30Correcting a delta normalization bug in VM (checked by benjamin)jforest
2008-09-25Forgot one file.msozeau
2008-09-25Improvements in coqdoc:msozeau
2008-09-25Various little improvements:msozeau
2008-09-25Partial fix for bug #1948: recompute order of dependencies betweenmsozeau
2008-09-16Report change of the implicit argument status of the carrier type in themsozeau
2008-09-15Report improvements in Equations to the dependent elimination tactic:msozeau
2008-09-15Fix bug #1943 and restrict the inference optimisation of Program tomsozeau
2008-09-15Add types introduced by subtac in *.glob filesglondu
2008-09-15Update stdlib html templateglondu
2008-09-14A pass on documentation: msozeau
2008-09-14Add user syntax for creating hint databases [Create HintDb foomsozeau
2008-09-14Use manual implicts in Classes and rationalize class parameter names.msozeau
2008-09-14In manual implicit arguments mode, do not enrich implicitsmsozeau
2008-09-14Fix bug #1931 by searching for a sort after doing beta,iota,delta-msozeau
2008-09-14Fix bug #1936: uncaught exception due to undefinable exceptions.msozeau
2008-09-14Fix bug #1939: defined evars were not substituted in some typeclassesmsozeau
2008-09-14Fix bug #1940: uncaught exception when searching for a type class.msozeau
2008-09-13Finish debugging the unification machinery in [Equations]. Do the _compmsozeau
2008-09-13Remove redefinition of id in Program.Basics, just add maximal implicits.msozeau
2008-09-13Fix a bug, in fold_constr_with_binders, the types of fixpoints weremsozeau
2008-09-12Add a type argument to letin_tac instead of using casts and recomputingmsozeau
2008-09-11Fixes in dependent induction tactic, putting things in better order formsozeau
2008-09-11Add enough information to correctly globalize recursive calls in inductive andmsozeau
2008-09-11Some more debugging of [Equations], unification still not perfect.msozeau
2008-09-10profondeur maximalefilliatr
2008-09-09added comments in esubst.mlibarras
2008-09-09Correction bug assert (introduit dans la révision 11300) qui neherbelin
2008-09-09Suppression d'un warning inutilenotin
2008-09-09Fix a bug reintroduced in [setoid_reflexivity] etc...msozeau
2008-09-07Commit fixes from v8.2 branch (r11386 and r11387)glondu
2008-09-07Generalize usage of $(FIND_VCS_CLAUSE) and add debian to itglondu
2008-09-07Do not install csdpcert in $(BINDIR)glondu
2008-09-07Check [Equations] patterns are for the right function.msozeau
2008-09-07Add the ability to declare [Hint Extern]'s with no pattern.msozeau
2008-09-07Fixes in typeclasses resolution. Avoid reducing instances types beforemsozeau
2008-09-07Update CHANGES and INSTALLglondu
2008-09-07Add some calls to $(STRIP) for consistencyglondu
2008-09-07$(DLLCOQRUN) is not an executableglondu
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-11 09:57:32 +0000