aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Suite commit 11539 sur notation Record dans (Co)Inductive (MAJGravatar herbelin2008-11-05
* Petit bug dans le commit précédent.Gravatar aspiwack2008-11-05
* Nouvelle syntaxe pour écrire des records (co)inductifs :Gravatar aspiwack2008-11-05
* Better extraction renaming phase (fix #1914 plus other non-reported bugs)Gravatar letouzey2008-11-05
* Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974)Gravatar herbelin2008-11-04
* 2 petites améliorations de coq_makefile (traitement des .ml4 + cibles géné...Gravatar notin2008-11-04
* Fix CAMLHLIB (due to r11358) (Closes: #1986)Gravatar glondu2008-11-02
* test-suite/ideal-features/{apply.v -> eapply_evar.v}Gravatar glondu2008-11-02
* Ajout d'une option -raw pour Coqdoc (sortie en texte brut)Gravatar notin2008-10-31
* allowed patternidents starting with an '_'Gravatar amahboub2008-10-31
* The lexer is changer to break former PATTERNIDENT into two tokens.Gravatar amahboub2008-10-30
* Document native "Declare ML Module"Gravatar glondu2008-10-29
* Remove calls to Dynlink.add_{interfaces,available_units} altogetherGravatar glondu2008-10-29
* Adaptation du vieil appel à "apply" sur lemme de symétrie au cas oùGravatar herbelin2008-10-29
* Oups...Gravatar notin2008-10-29
* Dépendance des cibles de la documentation envers les cibles de CoqGravatar notin2008-10-29
* Native "Declare ML Module" when possibleGravatar glondu2008-10-28
* petite modif du commit 11513.Gravatar soubiran2008-10-28
* 11511 continued (bug in set.out + incohérence dans "Theorem with"Gravatar herbelin2008-10-28
* Correction bug 1979.Gravatar soubiran2008-10-28
* - Fixed many "Theorem with" bugs.Gravatar herbelin2008-10-27
* Correct enormous bug in interpretation of generalized binders: it simplyGravatar msozeau2008-10-26
* Fixes and refinements regarding occurrence selection:Gravatar herbelin2008-10-26
* adding an option Function_raw_tcc to FunctionGravatar jforest2008-10-26
* Stop using a coqdocdoc env which prevents use of environments insideGravatar msozeau2008-10-26
* - MAJ svn:ignore pour bin/coq-parser (anciennement bin/parser)Gravatar herbelin2008-10-26
* Backtrack sur commit 11467 (tentative d'optimisation meta_instance quiGravatar herbelin2008-10-26
* More debugging of handling of open constrs with typeclasses:Gravatar msozeau2008-10-25
* Fix for bug #1981, correct the mismatch between the meta types used inGravatar msozeau2008-10-25
* Raise informative errors instead of Failures or anomalies in case a metaGravatar msozeau2008-10-24
* Fix doc of apply in (see coq-club message 26 September 2008)Gravatar herbelin2008-10-24
* Forgot one file which had other local modifications...Gravatar msozeau2008-10-23
* Fix bug #1977 by allowing the [apply] variants to take an [open_constr]Gravatar msozeau2008-10-23
* Open notation for declaring record instances.Gravatar msozeau2008-10-23
* Generalized implementation of generalization.Gravatar msozeau2008-10-23
* Fix bugs #1975 and #1976.Gravatar msozeau2008-10-22
* Fix for bug #1973 provided by Brian Campbell.Gravatar msozeau2008-10-22
* Various coqdoc improvements:Gravatar msozeau2008-10-22
* A much better implementation of implicit generalization:Gravatar msozeau2008-10-22
* Affichage des notations récursives:Gravatar herbelin2008-10-22
* More OCaml-3.11-friendly configure scriptGravatar glondu2008-10-21
* warning message when a qualid to extract can be both a module or a cstGravatar letouzey2008-10-21
* duplicated open of PpconstrGravatar letouzey2008-10-21
* Correction bug #1969.Gravatar soubiran2008-10-21
* Renommage "Global Instance" en "Instance Global" pour uniformisationGravatar herbelin2008-10-20
* Zdiv: eqm (equality modulo some N) can now be declared as Parametric RelationGravatar letouzey2008-10-20
* Syntaxe de COQBINGravatar notin2008-10-20
* Suite 11472 et 11473Gravatar herbelin2008-10-19
* Suite 11472Gravatar herbelin2008-10-19
* - Export de pattern_ident vers les ARGUMENT EXTEND and co.Gravatar herbelin2008-10-19