aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Préparation à la mise en place d'univers algébriquesGravatar herbelin2001-09-09
* Correction d'un bug de pretty-print.Gravatar clrenard2001-09-03
* Change la constante d'entree de ImmediateGravatar mohring2001-08-28
* ParsingGravatar herbelin2001-08-10
* Renommage TrueCut -> AssertGravatar herbelin2001-08-08
* La grammaire n'était plus LL1Gravatar herbelin2001-08-08
* Modification Tauto pour qu'il puisse destructurer des hypotheses de la formeGravatar courant2001-08-08
* Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ...Gravatar herbelin2001-08-07
* Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas s'a...Gravatar herbelin2001-08-05
* Elimination des coupures quand les 'clause' se réduisent à des hypothèses,...Gravatar herbelin2001-08-05
* Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas s'a...Gravatar herbelin2001-08-05
* Mise en place d'un nouveau Destruct sur le modèle du nouvel InductionGravatar herbelin2001-08-05
* Suppression des TmpHyp disgracieuses dans Decompose; utilisation de combinate...Gravatar herbelin2001-08-05
* Elimination des coupures quand les 'clause' se réduisent à des hypothèses,...Gravatar herbelin2001-08-05
* Ajout code pour un Destruct similaire au NewInductionGravatar herbelin2001-08-01
* Branchement de induction/destruct sur intros_until_n (intros_do obsolete ne p...Gravatar herbelin2001-07-13
* Branchement sur bad_tactic_argsGravatar herbelin2001-07-10
* Branchement sur bad_tactic_argsGravatar herbelin2001-07-10
* Ajout du .ml pour la tactique Setoid_replaceGravatar clrenard2001-07-10
* Changement de place de la tactique Setoid_rewrite et renommageGravatar clrenard2001-07-10
* ajout Show Intro(s)Gravatar letouzey2001-07-04
* Autoriser Apply avec un but sous forme d'implication ou de quantificationGravatar barras2001-06-29
* traitement du let dans red_product (tactique Red)Gravatar barras2001-06-29
* commit d'un bug de Apply.Gravatar barras2001-06-27
* Refine sur les CoFixGravatar filliatr2001-06-25
* Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...Gravatar herbelin2001-06-25
* Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...Gravatar herbelin2001-06-25
* Fix d'un bug de TautoGravatar delahaye2001-06-15
* Prise en compte env local (et defs locales) dans ChangeGravatar herbelin2001-06-13
* Correction d'un bug du a un Intros trop violentGravatar delahaye2001-06-01
* Backtrack vers comportement de la V6 pour eviter les globaux dans le nommage ...Gravatar herbelin2001-06-01
* Amelioration - subjective - de l'affichage des HintGravatar herbelin2001-05-31
* Pretty -> PrettypGravatar filliatr2001-05-28
* Remplacement push_rec_types (Rel) pour Fix parpush_named_rec_typesGravatar herbelin2001-05-25
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
* Changement de la structure des points fixesGravatar barras2001-05-03
* Ajout du cas True->A|-BGravatar delahaye2001-04-24
* Fonction lookup enleveeGravatar delahaye2001-04-19
* Mise en pageGravatar herbelin2001-04-15
* Ajout de _ dans les patterns d'introGravatar mohring2001-04-12
* Mis un message d'erreur explicite pour l'echec de Elim en casGravatar mohring2001-04-12
* Make it possible to perform proofs by induction even on non-inductive types,Gravatar bertot2001-04-03
* amelioration de la structure des universGravatar barras2001-03-28
* Problèmes de NewInductionGravatar herbelin2001-03-22
* entetesGravatar filliatr2001-03-15
* bug de refine: uncaught exception Array.subGravatar barras2001-03-09
* changement comparaison etatsGravatar filliatr2001-03-08
* Modification de e_give_exact pour eviter d'echouer sur l'unificationGravatar mohring2001-03-06
* eta-expansionGravatar mohring2001-03-06
* EAutod (debug)Gravatar filliatr2001-03-06