aboutsummaryrefslogtreecommitdiff
path: root/tactics/wcclausenv.ml
AgeCommit message (Expand)Author
2000-11-23print_id, print_sp -> pr_id, pr_spherbelin
2000-11-02suppression des (* open Generic *)filliatr
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec sorts)...herbelin
2000-10-18Renommage canonique :herbelin
2000-10-11C'était pas le bon env dans build_termherbelin
2000-09-12Modification mkAppL; abstraction via kind_of_term; changement dans Reductionherbelin
2000-09-10Correction pour make docherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-05-31Nettoyage de Genericherbelin
2000-05-18suppression ligne etrangeherbelin
2000-05-18ciseauxherbelin
2000-05-16Retrait du i pour tclTHEN_i et correction bugs Decomposeherbelin
2000-01-21gros commit de tout ce que j'ai fait pendant les vacances :filliatr
1999-12-01 - environment -> safe_environmentfilliatr
1999-11-25typage des existentielles dans Typing_ev; suppression metamap inutiles dans t...filliatr
1999-11-22module Wcclausenvfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 00:27:52 +0000