aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2008-10-20Renommage "Global Instance" en "Instance Global" pour uniformisationherbelin
2008-10-20Zdiv: eqm (equality modulo some N) can now be declared as Parametric Relationletouzey
2008-10-20Syntaxe de COQBINnotin
2008-10-19Suite 11472 et 11473herbelin
2008-10-19Suite 11472herbelin
2008-10-19- Export de pattern_ident vers les ARGUMENT EXTEND and co.herbelin
2008-10-19Retour en arrière sur la mise en paramètre du premier argument deherbelin
2008-10-19Retour en arrière pour raison de compatibilité sur la suppression du nf_evar herbelin
2008-10-18Fixed bug #1966, wrong handling of evars.msozeau
2008-10-18Optimisation de clenv.ml pour que meta_instance ne soit pas appeléherbelin
2008-10-18Expérience de simplification de Ndigits compte tenu des tactiques existantherbelin
2008-10-18- Merge modifs coq_makefile.ml4 de la 8.1 vers le trunk (commit 11429)herbelin
2008-10-18Que Time n'empêche pas la colorisation des mots-clés.herbelin
2008-10-18Intégration et formattage du développement de Pierre Castéran sur lesherbelin
2008-10-17Suppression de la dépendance de install-doc envers doc :notin
2008-10-16Extraction of Module with eq = ... : fix for bug #1853letouzey
2008-10-16Extraction of mutual types with alias: fix for bug #1965letouzey
2008-10-16Attempt to clarify Extract_env.extract_seb_specletouzey
2008-10-15Report des commits 11417 et 11437 de la v8.2soubiran
2008-10-14report de la révision r11451 (nouveau style html pour le manuel de référence)notin
2008-10-14Dumpglob.dump_modref : fix an assert failureletouzey
2008-10-14test-suite: more utf8 tests, a test of ! ? and so on in rewritesletouzey
2008-10-14ugly comment erroneously left in the minus definitionletouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 19:49:15 +0000