aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
Commit message (Expand)AuthorAge
* Application du patch de Michel Mauny pour pouvoir compiler en ocaml 3.08.1Gravatar herbelin2004-08-24
* Setoid_replace.setoid_replace: last argument (that was supposed to beGravatar sacerdot2004-07-23
* "Show Setoids" command added.Gravatar sacerdot2004-07-23
* correction d'un bug de la tactique pour les semi setoid rings.Gravatar clrenard2004-07-22
* Protection des accès tableau car, sur Sparc-linux, cela engendre une erreur ...Gravatar herbelin2004-07-19
* Abstraction vis a vis du type loc pour ocaml 3.08Gravatar herbelin2004-07-18
* Nouvelle en-têteGravatar herbelin2004-07-16
* ajout des unsafeCoerce + 2 bugs haskellGravatar letouzey2004-07-14
* * <style>...</style> tag no longer generated for theory filesGravatar sacerdot2004-07-08
* - recent changes to doubleTypeInference.ml (that introduced doubleGravatar sacerdot2004-07-08
* Commit to perform double type inference also on inner types.Gravatar sacerdot2004-07-08
* Constants just after a "Let id : t. ... Qed" local variable declaration wereGravatar sacerdot2004-07-05
* updated printing of evar context (may loop ?)Gravatar corbinea2004-06-30
* moved instantiate binding to extratacticsGravatar corbinea2004-06-29
* License de contrib/interfaceGravatar herbelin2004-06-29
* contrib/interface *$*$@!Gravatar corbinea2004-06-28
* Modules et Records: gros changements pour prendre en compte le nouveau mind_r...Gravatar letouzey2004-06-28
* Licence changed from GPL to Lesser GPL.Gravatar sacerdot2004-06-26
* eq and eqT are the sameGravatar barras2004-06-25
* correspondance des records et noms de champs de records entre un module et sa...Gravatar letouzey2004-06-25
* Retour sur amendement de l'interprétation mult sur nat (bug 743) car incompa...Gravatar herbelin2004-05-28
* "comments only" commit.Gravatar coq2004-05-13
* Correction interprétation mult sur nat (bug 743), bug Oufo (mais Oufo est de...Gravatar herbelin2004-05-07
* pb install de pcoqGravatar barras2004-04-21
* Copyright notice of files in contrib/xml made uniform.Gravatar sacerdot2004-04-07
* Old file. The new version of this script is no longer distributed withGravatar sacerdot2004-04-07
* - theoryobject.dtd is the DTD for .theory filesGravatar sacerdot2004-04-07
* Loic code to pretty-print the generated proof-tree debranched (since itGravatar sacerdot2004-04-07
* CoRN CProp detection improved: products of "sort" CProp are now recognizedGravatar sacerdot2004-04-07
* Coqdoc backtrack: HTML special characters are no longer quoted inside # ... #;Gravatar sacerdot2004-04-07
* Fake dependent products in inductive definition types are no longer replacedGravatar sacerdot2004-04-06
* Important bug fix: since coqdoc is now quoting XML reserved characters inGravatar sacerdot2004-04-06
* Since coqdoc produces (X)HTML, HTML character entities can be usedGravatar sacerdot2004-04-05
* correction rapide du bug PR\#592Gravatar letouzey2004-04-05
* ** WARNING **Gravatar sacerdot2004-04-04
* LocalFact added as a choice for the "as" attribute of ht:VARIABLE in theGravatar sacerdot2004-04-01
* Big bug fixed: interactive local definitions where handled as constantsGravatar sacerdot2004-04-01
* Output of theory files reimplemented using Buffer.Gravatar sacerdot2004-04-01
* ~keep_sections was now redundant. Got rid of.Gravatar sacerdot2004-04-01
* En mode batch, recuperation via Declare de l'information si un inductive est ...Gravatar herbelin2004-03-31
* Fake dependent types in constructors of inductive types are now preserved.Gravatar sacerdot2004-03-31
* *** WARNING: DTD Change ***Gravatar sacerdot2004-03-30
* declare_internal_constant behaved as declare_constant for proofs (e.g.Gravatar sacerdot2004-03-30
* No longer used (and probably no longer working) code removed.Gravatar sacerdot2004-03-30
* Added a <br/> after "Require ...".Gravatar sacerdot2004-03-30
* syntax error: dandling inGravatar sacerdot2004-03-30
* RenommageGravatar herbelin2004-03-30
* 2 choix incorrectsGravatar herbelin2004-03-30
* Distinction entre declarations internes (p.ex. _subproof) et declarations uti...Gravatar herbelin2004-03-30
* Fabrication de l'uri a partir du path utilisateurGravatar herbelin2004-03-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 01:08:05 +0000