aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Code redondantGravatar herbelin2000-10-13
* Code redondantGravatar herbelin2000-10-13
* Renommage des find_m*typeGravatar herbelin2000-10-11
* Suppression d'un Cast inutileGravatar herbelin2000-10-05
* Utilisation de local_strong plutôt que strong buggé avec défs locales (2ème)Gravatar herbelin2000-10-04
* Utilisation de local_strong plutôt que strong buggé avec défs localesGravatar herbelin2000-10-04
* Ajout LetIn dans prim_extractorGravatar herbelin2000-10-04
* Elimination des coupures sur le type constantGravatar herbelin2000-10-04
* Ajout castedopenconstrargGravatar herbelin2000-10-03
* Rebranchement de la tactique LetGravatar herbelin2000-10-03
* Renommage AppL en AppGravatar herbelin2000-10-01
* Plus de whd_castappGravatar herbelin2000-10-01
* Plus de whd_castapp_stackGravatar herbelin2000-10-01
* Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d...Gravatar herbelin2000-09-26
* Abstraction de constrGravatar herbelin2000-09-14
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* Correction pour make docGravatar herbelin2000-09-10
* Suppression de AbstGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Pattern matching de sous-termesGravatar delahaye2000-08-17
* retablissement make doc et make minicoqGravatar filliatr2000-07-25
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Passage à des contextes de vars et de rels pouvant contenir des déclaration...Gravatar herbelin2000-07-24
* Pattern -> parsingGravatar delahaye2000-07-21
* Modifs d'interpretation de patternsGravatar delahaye2000-07-21
* portage RefineGravatar filliatr2000-07-20
* Correction de CofixGravatar delahaye2000-07-03
* Extension de find_inductive aux co-inductifs et renommage en find_rectypeGravatar herbelin2000-07-01
* RienGravatar herbelin2000-06-29
* Modifs de presentation.Gravatar delahaye2000-06-28
* portage EAuto et RingGravatar filliatr2000-06-21
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* Nettoyage de GenericGravatar herbelin2000-05-31
* Déplacement de save_thm and co de PFedit vers CommandGravatar herbelin2000-05-25
* Bug existential_value au lieu de existential_type + divers sur existentialGravatar herbelin2000-05-25
* DocGravatar herbelin2000-05-23
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* bug (typage avec meta)Gravatar herbelin2000-05-18
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18
* docGravatar herbelin2000-05-18
* Retrait du i pour tclTHEN_i et correction bugs DecomposeGravatar herbelin2000-05-16
* Achèvement nettoyage PfeditGravatar herbelin2000-05-05
* Nettoyage de l'interface de PfeditGravatar herbelin2000-05-04
* compilation bytecode / native :Gravatar filliatr2000-05-03
* Completion d'un match non exhaustifGravatar delahaye2000-05-03
* diverses modifs pour ocamlwebGravatar filliatr2000-05-03
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* portage Omega (mais toujours pas Zpower et Zlogarithm)Gravatar filliatr2000-05-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 15:20:14 +0000