aboutsummaryrefslogtreecommitdiff
path: root/proofs/logic.ml
AgeCommit message (Expand)Author
2002-06-13Bug non vérification non redondance par Cutherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-04-12q: Commande introuvable.herbelin
2002-03-27Simplification de Proof_type.prim_ruleherbelin
2002-03-07Clear ne substitue plus le corps dans le reste du butbarras
2002-02-28Uniformisation convert_hypherbelin
2002-02-22suppression de pop_namedbarras
2002-02-15petits changements cosmetiques sur les tactiquesbarras
2002-02-08prterm -> prterm_envfilliatr
2002-02-07petit nettoyage de kernel/inductivebarras
2002-02-01Ajout tactiques Rename et Pose; modifications pour Inversionherbelin
2001-12-13compat ocaml 3.03filliatr
2001-11-29nouvel algo de conversion plus uniformebarras
2001-11-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
2001-11-06Suppression des local_constraints, des ctxtty et du focus.clrenard
2001-11-05GROS COMMIT:barras
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-10-05Petit oubli à propos de ThinBodyherbelin
2001-10-05Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle...herbelin
2001-08-08Ajout nf_betaiota dans le cut interneherbelin
2001-08-07Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ...herbelin
2001-06-25Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...herbelin
2001-05-23amelioration des messages d'erreurs vis a vis des evarsbarras
2001-05-03Changement de la structure des points fixesbarras
2001-04-14Reparation du bug de Trydelahaye
2001-03-28amelioration de la structure des universbarras
2001-03-15entetesfilliatr
2001-02-28introduction d'un refine avec resolution des types et de l'instantiation des ...mohring
2001-02-01*** empty log message ***mohring
2000-12-06Ajout erreur DoesNotOccurInherbelin
2000-11-23print_id, print_sp -> pr_id, pr_spherbelin
2000-11-02correction Abstract (et make world passe!)filliatr
2000-11-02suppression des (* open Generic *)filliatr
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec sorts)...herbelin
2000-10-18Renommage canonique :herbelin
2000-10-11Renommage des find_m*typeherbelin
2000-10-05Suppression d'un Cast inutileherbelin
2000-10-04Ajout LetIn dans prim_extractorherbelin
2000-10-03Rebranchement de la tactique Letherbelin
2000-10-01Renommage AppL en Appherbelin
2000-10-01Plus de whd_castappherbelin
2000-09-14Abstraction de constrherbelin
2000-09-12Modification mkAppL; abstraction via kind_of_term; changement dans Reductionherbelin
2000-09-10Correction pour make docherbelin
2000-09-10Suppression de Abstherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclaration...herbelin
2000-07-03Correction de Cofixdelahaye
2000-07-01Extension de find_inductive aux co-inductifs et renommage en find_rectypeherbelin
2000-06-29Rienherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 12:31:06 +0000