aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/refiner.ml
Commit message (Expand)AuthorAge
...
* Retrait du i pour tclTHEN_i et correction bugs DecomposeGravatar herbelin2000-05-16
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* Correction bug des réduction 'deltat' et renommage 'deltat' en 'evar'Gravatar herbelin2000-03-17
* MAJ ocaml 2.99 (espaces dans la syntaxe des cast)Gravatar herbelin2000-01-26
* Abstraction de l'implémentation des signatures de Sign en vue intégration d...Gravatar herbelin2000-01-26
* rattrapage exceptions autres que UserErrorGravatar filliatr1999-12-14
* mise a jour de refiner.ml (reports de modifs de la V6.3)Gravatar barras1999-12-13
* - états fabriqués avec -silentGravatar filliatr1999-12-13
* modifs pour premiere edition de liensGravatar filliatr1999-12-02
* module PfeditGravatar filliatr1999-12-01
* - Typing -> Safe_typingGravatar filliatr1999-12-01
* typage des existentielles dans Typing_ev; suppression metamap inutiles dans t...Gravatar filliatr1999-11-25
* module RefinerGravatar filliatr1999-10-19
* les variables existentielles contiennent maintenant un environnement (typeGravatar filliatr1999-10-19
* mise en place module RefinerGravatar filliatr1999-10-18
* - déplacement (encore une fois !) des variables existentielles : elles sontGravatar filliatr1999-10-18