aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/equality.ml
Commit message (Expand)AuthorAge
* Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...Gravatar herbelin2001-02-14
* code mortGravatar herbelin2001-02-07
* Bug confusion existS/sigSGravatar herbelin2000-12-25
* LetIn dans SimplGravatar mohring2000-12-14
* Portage d'AutoRewriteGravatar delahaye2000-12-02
* Nouveau long long avec Coq en têteGravatar herbelin2000-11-29
* Prise en compte du repertoire dans le section path; utilisation de dirpath po...Gravatar herbelin2000-11-28
* Appel des constantes globaux par des noms absolusGravatar herbelin2000-11-26
* certains effets disparaissent a la sortie des sections, d'autres non (selon S...Gravatar filliatr2000-11-24
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...Gravatar herbelin2000-11-22
* PatternMatchingFailure n'etait pas rattrapeeGravatar herbelin2000-11-21
* Bugs make_tuple et existS_patternGravatar herbelin2000-11-21
* Remplacement des hacks pour les noms longs par un appel à Declare.global_qua...Gravatar herbelin2000-11-20
* methode exportGravatar filliatr2000-11-15
* Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...Gravatar herbelin2000-11-10
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Renommage canonique :Gravatar herbelin2000-10-18
* Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve...Gravatar herbelin2000-10-13
* Prise en compte de Let dans build_dependent_inductiveGravatar herbelin2000-10-11
* Correction incompatibilites dans la fn des types des inductifsGravatar herbelin2000-10-06
* Code mortGravatar herbelin2000-10-04
* code mortGravatar herbelin2000-10-04
* Renommage AppL en AppGravatar herbelin2000-10-01
* Elimination de coupures...Gravatar herbelin2000-10-01
* 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
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* 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
* portage EAuto et RingGravatar filliatr2000-06-21
* 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
* suppression de l'env/sigma dans les fonctions de reduction beta et iota seulsGravatar herbelin2000-05-22
* bugsGravatar herbelin2000-05-18
* NettoyageGravatar herbelin2000-05-18
* Retrait du i pour tclTHEN_i et correction bugs DecomposeGravatar herbelin2000-05-16
* Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)Gravatar herbelin2000-05-04
* MAJGravatar herbelin2000-05-03
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* 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
* 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
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-22 08:03:31 +0000