aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tauto.ml
Commit message (Expand)AuthorAge
* Moving tauto.ml4 to a proper ML file.Gravatar Pierre-Marie Pédrot2016-02-23
* Remplacement de Tauto et IntuitionGravatar delahaye2000-10-30
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve...Gravatar herbelin2000-10-13
* 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
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* 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
* Retrait du i pour tclTHEN_i et correction bugs DecomposeGravatar herbelin2000-05-16
* Problème avec motif du second-ordreGravatar herbelin2000-05-02
* Adaptés pour le type constr_pattern et les nouvelles fonctions de filtrageGravatar herbelin2000-04-30
* Introduction d'un type constr_pattern pour les différents filtragesGravatar herbelin2000-04-26
* erreurs lexicales dans les patterns (manquait des espaces)Gravatar filliatr2000-03-30
* - bug make_module_marker (plus de # et de .obj maintenant)Gravatar filliatr2000-03-21
* MAJ ocaml 2.99Gravatar herbelin2000-03-21
* TautoGravatar filliatr2000-03-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-24 13:59:58 +0000