aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Expand)Author
2004-12-09travail sur les types extraitsletouzey
2004-12-07* added subst_evaluable_referencesacerdot
2004-12-06Code mortherbelin
2004-12-06Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...herbelin
2004-12-03Orthographe!herbelin
2004-11-29Correction 1.138 appliquée à tort à la branche principale au lieu de V8-0b...herbelin
2004-11-29Commit précédent erroné; retour version précédenteherbelin
2004-11-28MAJ vis à vis de extratacticsherbelin
2004-11-18When a reference to a constructor is met its inductive type must be closed.sacerdot
2004-11-17Locate Moduleherbelin
2004-11-17New command "Print Rewrite HindDb dbname".sacerdot
2004-11-16Names.substitution (and related functions) and Term.subst_mps moved tosacerdot
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
2004-11-12Changement dans les boxed values .gregoire
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-10-11'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...herbelin
2004-10-11Suppression IsConjecture redondant avec Conjecturalherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 12:32:34 +0000