aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/wcclausenv.ml
Commit message (Expand)AuthorAge
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* C'était pas le bon env dans build_termGravatar herbelin2000-10-11
* 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
* Nettoyage de GenericGravatar herbelin2000-05-31
* suppression ligne etrangeGravatar herbelin2000-05-18
* ciseauxGravatar herbelin2000-05-18
* Retrait du i pour tclTHEN_i et correction bugs DecomposeGravatar herbelin2000-05-16
* gros commit de tout ce que j'ai fait pendant les vacances :Gravatar filliatr2000-01-21
* - environment -> safe_environmentGravatar filliatr1999-12-01
* typage des existentielles dans Typing_ev; suppression metamap inutiles dans t...Gravatar filliatr1999-11-25
* module WcclausenvGravatar filliatr1999-11-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 22:56:04 +0000