aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2008-10-2811511 continued (bug in set.out + incohérence dans "Theorem with"herbelin
2008-10-28Correction bug 1979.soubiran
2008-10-27- Fixed many "Theorem with" bugs.herbelin
2008-10-26Correct enormous bug in interpretation of generalized binders: it simplymsozeau
2008-10-26Fixes and refinements regarding occurrence selection:herbelin
2008-10-26adding an option Function_raw_tcc to Functionjforest
2008-10-26Stop using a coqdocdoc env which prevents use of environments insidemsozeau
2008-10-26- MAJ svn:ignore pour bin/coq-parser (anciennement bin/parser)herbelin
2008-10-26Backtrack sur commit 11467 (tentative d'optimisation meta_instance quiherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 12:29:39 +0000