| modules Indrec, Wcclausenv; progression dans Tacticals |
|
More...
|
about 26 years ago
|
| module Pattern, Wcclausenv (interface) et Tacticals |
|
More...
|
about 26 years ago
|
| modules Bij, Gmapl, Stock |
|
More...
|
about 26 years ago
|
| Version pr��liminaire |
|
More...
|
about 26 years ago
|
| discriminations nets |
|
More...
|
about 26 years ago
|
| introduction de Gset et Gmap pour Tlm puis Dn |
|
More...
|
about 26 years ago
|
| Sets et Maps avec egalite generique |
|
More...
|
about 26 years ago
|
| pas de grosse banniere; pas de double point-virguke |
|
More...
|
about 26 years ago
|
| On se fait la main: plus de precision si ill-formed rec body |
|
More...
|
about 26 years ago
|
| Traducteur ast -> rawterm |
|
More...
|
about 26 years ago
|
| Type ML des termes non pr��typ��s |
|
More...
|
about 26 years ago
|
| - r��pertoire tactics/ - discrimination nets (d��but) : modules Tlm et Dn |
|
More...
|
about 26 years ago
|
| module Macros et Tacinterp |
|
More...
|
about 26 years ago
|
| - module Redinfo dans library/ pour les constantes d'��limination - module Tacred : fonctions de reductions utilisees dans les tactiques |
|
More...
|
about 26 years ago
|
| - documentation repertoire proofs/ - IsAppL of constr * constr list ==> r��percussion - module Clenv (suite; as termin��) |
|
More...
|
about 26 years ago
|
| documentation proofs |
|
More...
|
about 26 years ago
|
| module Clenv (debut) |
|
More...
|
about 26 years ago
|
| modules Evar_refiner et Typing_ev |
|
More...
|
about 26 years ago
|
| module Refiner |
|
More...
|
about 26 years ago
|
| les variables existentielles contiennent maintenant un environnement (type unsafe_env) et non pas seulement une signature. Le module Evd vient donc apres le module Environ. |
|
More...
|
about 26 years ago
|
| mise en place module Refiner |
|
More...
|
about 26 years ago
|
| - d��placement (encore une fois !) des variables existentielles : elles sont toujours dans le noyau (en ce sens que Reduction et Typeops les connaissent) mais dans un argument suppl��mentaire A COTE de l'environnement (de type unsafe_env) - Indtypes et Typing n'utilisent strictement que Evd.empty |
|
More...
|
about 26 years ago
|
| module Logic |
|
More...
|
about 26 years ago
|
| module Proof_trees |
|
More...
|
about 26 years ago
|
| pas de merge univers dans Declare, car deja fait dans Environ |
|
More...
|
about 26 years ago
|
| organisation de trad (entre parsing/ et pretyping/) |
|
More...
|
about 26 years ago
|
| mise a jour |
|
More...
|
about 26 years ago
|
| plus de recettes pour les corps des constantes |
|
More...
|
about 26 years ago
|
| - re-introduction d'une evar_map dans unsafe_env - les var. ex. sont des entiers, et non plus des section_path |
|
More...
|
about 26 years ago
|
| documentation |
|
More...
|
about 26 years ago
|
