aboutsummaryrefslogtreecommitdiff
path: root/proofs/refiner.ml
AgeCommit message (Expand)Author
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-07-21Modifs d'interpretation de patternsdelahaye
2000-05-16Retrait du i pour tclTHEN_i et correction bugs Decomposeherbelin
2000-05-03Ajout du langage de tactiquesdelahaye
2000-03-17Correction bug des réduction 'deltat' et renommage 'deltat' en 'evar'herbelin
2000-01-26MAJ ocaml 2.99 (espaces dans la syntaxe des cast)herbelin
2000-01-26Abstraction de l'implémentation des signatures de Sign en vue intégration d...herbelin
1999-12-14rattrapage exceptions autres que UserErrorfilliatr
1999-12-13mise a jour de refiner.ml (reports de modifs de la V6.3)barras
1999-12-13 - états fabriqués avec -silentfilliatr
1999-12-02modifs pour premiere edition de liensfilliatr
1999-12-01module Pfeditfilliatr
1999-12-01 - Typing -> Safe_typingfilliatr
1999-11-25typage des existentielles dans Typing_ev; suppression metamap inutiles dans t...filliatr
1999-10-19module Refinerfilliatr
1999-10-19les variables existentielles contiennent maintenant un environnement (typefilliatr
1999-10-18mise en place module Refinerfilliatr
1999-10-18 - déplacement (encore une fois !) des variables existentielles : elles sontfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 19:22:21 +0000