aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Expand)Author
2004-10-04un paquet de corrections de bugsletouzey
2004-10-01The "Add Setoid" command now has a new argument "as name" that is usedsacerdot
2004-09-30cutrewrite does not work with relations that are not Coq-like equalities.sacerdot
2004-09-29New syntaxsacerdot
2004-09-27firstorder bugfix to cope with elim of sigma types with goal is of the wrong ...corbinea
2004-09-17restructuration des printers: proofs passe avant parsingbarras
2004-09-15hiding the meta_map in evar_defsbarras
2004-09-12inclusion de meta_map dans evar_defsbarras
2004-09-09Ajout de or-pattern pour le match-with v8herbelin
2004-09-08The innersort is now computed as the more precise sort between thesacerdot
2004-09-08The code used to compare the synthesized and the expected type (if available)sacerdot
2004-09-07deuxieme vague de modifs: evar_defs fonctionnelbarras
2004-09-06reparation des Extract Constant avec Haskellletouzey
2004-09-03premiere reorganisation de l\'unificationbarras
2004-09-03Ported to the new implementation of setoid_*.sacerdot
2004-09-03The old implementation of (setoid_replace c1 with c2) used to replacesacerdot
2004-08-24Application du patch de Michel Mauny pour pouvoir compiler en ocaml 3.08.1herbelin
2004-07-23Setoid_replace.setoid_replace: last argument (that was supposed to besacerdot
2004-07-23"Show Setoids" command added.sacerdot
2004-07-22correction d'un bug de la tactique pour les semi setoid rings.clrenard
2004-07-19Protection des accès tableau car, sur Sparc-linux, cela engendre une erreur ...herbelin
2004-07-18Abstraction vis a vis du type loc pour ocaml 3.08herbelin
2004-07-16Nouvelle en-têteherbelin
2004-07-14ajout des unsafeCoerce + 2 bugs haskellletouzey
2004-07-08* <style>...</style> tag no longer generated for theory filessacerdot
2004-07-08- recent changes to doubleTypeInference.ml (that introduced doublesacerdot
2004-07-08Commit to perform double type inference also on inner types.sacerdot
2004-07-05Constants just after a "Let id : t. ... Qed" local variable declaration weresacerdot
2004-06-30updated printing of evar context (may loop ?)corbinea
2004-06-29moved instantiate binding to extratacticscorbinea
2004-06-29License de contrib/interfaceherbelin
2004-06-28contrib/interface *$*$@!corbinea
2004-06-28Modules et Records: gros changements pour prendre en compte le nouveau mind_r...letouzey
2004-06-26Licence changed from GPL to Lesser GPL.sacerdot
2004-06-25eq and eqT are the samebarras
2004-06-25correspondance des records et noms de champs de records entre un module et sa...letouzey
2004-05-28Retour sur amendement de l'interprétation mult sur nat (bug 743) car incompa...herbelin
2004-05-13"comments only" commit.coq
2004-05-07Correction interprétation mult sur nat (bug 743), bug Oufo (mais Oufo est de...herbelin
2004-04-21pb install de pcoqbarras
2004-04-07Copyright notice of files in contrib/xml made uniform.sacerdot
2004-04-07Old file. The new version of this script is no longer distributed withsacerdot
2004-04-07- theoryobject.dtd is the DTD for .theory filessacerdot
2004-04-07Loic code to pretty-print the generated proof-tree debranched (since itsacerdot
2004-04-07CoRN CProp detection improved: products of "sort" CProp are now recognizedsacerdot
2004-04-07Coqdoc backtrack: HTML special characters are no longer quoted inside # ... #;sacerdot
2004-04-06Fake dependent products in inductive definition types are no longer replacedsacerdot
2004-04-06Important bug fix: since coqdoc is now quoting XML reserved characters insacerdot
2004-04-05Since coqdoc produces (X)HTML, HTML character entities can be usedsacerdot
2004-04-05correction rapide du bug PR\#592letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 16:46:27 +0000