aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* RienGravatar herbelin2000-06-29
* Modifs de presentation.Gravatar delahaye2000-06-28
* bug discharge STRUCTURE; FrozenState supprimmes dans les ClosedSection -> .vo...Gravatar filliatr2000-06-21
* portage EAuto et RingGravatar filliatr2000-06-21
* Code mortGravatar herbelin2000-06-15
* Retrait des lam_and_pop and co (2ème - bug)Gravatar herbelin2000-06-03
* Retrait des lam_and_pop and coGravatar herbelin2000-06-03
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-02
* Nettoyage de GenericGravatar herbelin2000-05-31
* Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeursGravatar herbelin2000-05-31
* Déplacement de save_thm and co de PFedit vers CommandGravatar herbelin2000-05-25
* Bug stupide d'ordre d'évaluationGravatar herbelin2000-05-23
* suppression de l'env/sigma dans les fonctions de reduction beta et iota seulsGravatar herbelin2000-05-22
* Changement nommage des hypothèsesGravatar herbelin2000-05-22
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* Retour comportement de la version précédenteGravatar herbelin2000-05-22
* bugsGravatar herbelin2000-05-18
* suppression ligne etrangeGravatar herbelin2000-05-18
* ciseauxGravatar herbelin2000-05-18
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18
* NettoyageGravatar herbelin2000-05-18
* Retrait du i pour tclTHEN_i et correction bugs DecomposeGravatar herbelin2000-05-16
* RienGravatar herbelin2000-05-16
* Achèvement nettoyage Pfedit; ajout intros_replacingGravatar herbelin2000-05-05
* Intégration de leminvGravatar herbelin2000-05-05
* les erreursGravatar herbelin2000-05-04
* Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)Gravatar herbelin2000-05-04
* Nettoyage de l'interface de PfeditGravatar herbelin2000-05-04
* Reparation du bug d'interpretation d'AbstractGravatar delahaye2000-05-03
* diverses modifs pour ocamlwebGravatar filliatr2000-05-03
* MAJGravatar herbelin2000-05-03
* Ajout get_referenceGravatar herbelin2000-05-03
* Encapsulage de PatternMatchingFailure par un 'error' pour que l'echec de conc...Gravatar herbelin2000-05-03
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* DiversGravatar herbelin2000-05-02
* Problème avec motif du second-ordreGravatar herbelin2000-05-02
* Suite intégration de constr_patternGravatar herbelin2000-04-30
* Intégration progressiveGravatar herbelin2000-04-30
* Adaptés pour le type constr_pattern et les nouvelles fonctions de filtrageGravatar herbelin2000-04-30
* Déplacement du type reference dans TermGravatar herbelin2000-04-28
* Déplacement du type reference dans TermGravatar herbelin2000-04-28
* Decoupage de tactics/pattern en proofs/pattern et tactics/hipatternGravatar herbelin2000-04-28
* Changement de représentation du contexte des réf dans rawconstr et patternGravatar herbelin2000-04-28
* Introduction d'un type constr_pattern pour les différents filtragesGravatar herbelin2000-04-26
* NettoyageGravatar herbelin2000-04-26
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
* erreurs lexicales dans les patterns (manquait des espaces)Gravatar filliatr2000-03-30
* Nettoyage de l'interface d'Astterm; renommage des {pf_,}constr_of_com* en {pf...Gravatar herbelin2000-03-28
* Inversion (pas termine)Gravatar filliatr2000-03-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 18:15:31 +0000