aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2008-10-25More debugging of handling of open constrs with typeclasses:msozeau
2008-10-25Fix for bug #1981, correct the mismatch between the meta types used inmsozeau
2008-10-24Raise informative errors instead of Failures or anomalies in case a metamsozeau
2008-10-24Fix doc of apply in (see coq-club message 26 September 2008)herbelin
2008-10-23Forgot one file which had other local modifications...msozeau
2008-10-23Fix bug #1977 by allowing the [apply] variants to take an [open_constr]msozeau
2008-10-23Open notation for declaring record instances.msozeau
2008-10-23Generalized implementation of generalization.msozeau
2008-10-22Fix bugs #1975 and #1976.msozeau
2008-10-22Fix for bug #1973 provided by Brian Campbell.msozeau
2008-10-22Various coqdoc improvements:msozeau
2008-10-22A much better implementation of implicit generalization:msozeau
2008-10-22Affichage des notations récursives:herbelin
2008-10-21More OCaml-3.11-friendly configure scriptglondu
2008-10-21warning message when a qualid to extract can be both a module or a cstletouzey
2008-10-21duplicated open of Ppconstrletouzey
2008-10-21Correction bug #1969.soubiran
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 00:47:54 +0000