aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2008-11-07Slight change of the semantics of user-given casts: they don't reallymsozeau
2008-11-07- Ajout possibilité de lancer ocamldebug sur coqideherbelin
2008-11-07Suite #11533notin
2008-11-07Correction du bug #1926notin
2008-11-07Add some example uses of the new record features in Record.v:msozeau
2008-11-07Fix a bug in the specialization by unification tactic related to the problemsmsozeau
2008-11-07Add the ability to give a specific tactic to solve each obligation inmsozeau
2008-11-07Fix universe problem appearing ConCaT using the existing infrastructure formsozeau
2008-11-06Cosmetic: no more whitespace at end of lines in extraction filesletouzey
2008-11-06Correction d'un petit bug en cas de redéfintion par l'utilisateur de variabl...notin
2008-11-05Minor fixes:msozeau
2008-11-05Port [rewrite] tactics to open terms. Currently no check that evarsmsozeau
2008-11-05Fix in the unification algorithm using evars: unify types of evarmsozeau
2008-11-05Move Record desugaring to constrintern and add ability to use notationsmsozeau
2008-11-05Suite commit 11539 sur notation Record dans (Co)Inductive (MAJherbelin
2008-11-05Petit bug dans le commit précédent.aspiwack
2008-11-05Nouvelle syntaxe pour écrire des records (co)inductifs :aspiwack
2008-11-05Better extraction renaming phase (fix #1914 plus other non-reported bugs)letouzey
2008-11-04Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974)herbelin
2008-11-042 petites améliorations de coq_makefile (traitement des .ml4 + cibles géné...notin
2008-11-02Fix CAMLHLIB (due to r11358) (Closes: #1986)glondu
2008-11-02test-suite/ideal-features/{apply.v -> eapply_evar.v}glondu
2008-10-31Ajout d'une option -raw pour Coqdoc (sortie en texte brut)notin
2008-10-31allowed patternidents starting with an '_'amahboub
2008-10-30The lexer is changer to break former PATTERNIDENT into two tokens.amahboub
2008-10-29Document native "Declare ML Module"glondu
2008-10-29Remove calls to Dynlink.add_{interfaces,available_units} altogetherglondu
2008-10-29Adaptation du vieil appel à "apply" sur lemme de symétrie au cas oùherbelin
2008-10-29Oups...notin
2008-10-29Dépendance des cibles de la documentation envers les cibles de Coqnotin
2008-10-28Native "Declare ML Module" when possibleglondu
2008-10-28petite modif du commit 11513.soubiran
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 11:22:26 +0000