aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/inv.ml
Commit message (Expand)AuthorAge
* Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...Gravatar herbelin2001-02-14
* Command -> ConstrGravatar herbelin2000-12-25
* Bug Inversion en présence de méta-variablesGravatar herbelin2000-12-13
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Renommage canonique :Gravatar herbelin2000-10-18
* Prise en compte de Let à certains endroitsGravatar herbelin2000-10-11
* Bug ordre dans push_relsGravatar herbelin2000-10-10
* Code mortGravatar herbelin2000-10-01
* Abstraction de constrGravatar herbelin2000-09-14
* 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
* 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
* Retrait des lam_and_pop and coGravatar herbelin2000-06-03
* 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
* Intégration de leminvGravatar herbelin2000-05-05
* les erreursGravatar herbelin2000-05-04
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* Intégration progressiveGravatar herbelin2000-04-30
* Inversion (pas termine)Gravatar filliatr2000-03-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-21 21:54:16 +0000