aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Expand)Author
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
2004-04-04** WARNING **sacerdot
2004-04-01LocalFact added as a choice for the "as" attribute of ht:VARIABLE in thesacerdot
2004-04-01Big bug fixed: interactive local definitions where handled as constantssacerdot
2004-04-01Output of theory files reimplemented using Buffer.sacerdot
2004-04-01~keep_sections was now redundant. Got rid of.sacerdot
2004-03-31En mode batch, recuperation via Declare de l'information si un inductive est ...herbelin
2004-03-31Fake dependent types in constructors of inductive types are now preserved.sacerdot
2004-03-30*** WARNING: DTD Change ***sacerdot
2004-03-30declare_internal_constant behaved as declare_constant for proofs (e.g.sacerdot
2004-03-30No longer used (and probably no longer working) code removed.sacerdot
2004-03-30Added a <br/> after "Require ...".sacerdot
2004-03-30syntax error: dandling insacerdot
2004-03-30Renommageherbelin
2004-03-302 choix incorrectsherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 21:20:52 +0000