aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/refiner.ml
Commit message (Expand)AuthorAge
* introduction d'un refine avec resolution des types et de l'instantiation des ...Gravatar mohring2001-02-28
* simplification du make depend; fonctions de stat. util. memoire dans certains...Gravatar filliatr2001-02-08
* Remplacement de debug en assertGravatar herbelin2000-12-25
* Bug norm_evar_pf; remplacement par l'insertion d'un noeud local_constraints q...Gravatar herbelin2000-12-20
* Hint Unfold Local + commentairesGravatar mohring2000-12-12
* Portage d'AutoRewriteGravatar delahaye2000-12-02
* correction Abstract (et make world passe!)Gravatar filliatr2000-11-02
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Essai de remplacement du whd_betaiotaevar de Qed par un whd_iseGravatar herbelin2000-10-26
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Code redondantGravatar herbelin2000-10-13
* Utilisation de local_strong plutôt que strong buggé avec défs locales (2ème)Gravatar herbelin2000-10-04
* Utilisation de local_strong plutôt que strong buggé avec défs localesGravatar herbelin2000-10-04
* 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
* Modifs d'interpretation de patternsGravatar delahaye2000-07-21
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-22 08:52:07 +0000