aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* cosmétiqueGravatar herbelin2000-08-28
* messages d'erreurGravatar herbelin2000-07-28
* Plus de piquants dans les actions des grammaires; nom de la grammaire pris co...Gravatar herbelin2000-07-28
* 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
* Modifs d'interpretation de patternsGravatar delahaye2000-07-21
* portage RefineGravatar filliatr2000-07-20
* Plus de env et sigma dans get_arity, plus de sigma dans make_arityGravatar herbelin2000-07-01
* 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 02:52:28 +0000