aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/environ.ml
Commit message (Expand)AuthorAge
* nouvelle implantation de la reductionGravatar barras2001-03-01
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* simplification du make depend; fonctions de stat. util. memoire dans certains...Gravatar filliatr2001-02-08
* Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refGravatar herbelin2001-02-07
* Export de it_mkProd_or_LetIn_name et it_mkLambda_or_LetIn_nameGravatar herbelin2000-12-18
* Ajout de evaluable_named_decl et evaluable_rel_decl en parallele au evaluable...Gravatar herbelin2000-11-27
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* Ajout push_rels_assumGravatar herbelin2000-11-23
* Ajout sp_of_global; Introduction constant_path = section_pathGravatar herbelin2000-11-20
* Code more concernant feu les abstractionsGravatar herbelin2000-11-11
* Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...Gravatar herbelin2000-11-06
* nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...Gravatar filliatr2000-11-06
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Ajout push_rec_typesGravatar herbelin2000-10-11
* Elimination des coupures sur le type constantGravatar herbelin2000-10-04
* Rebranchement de la tactique LetGravatar herbelin2000-10-03
* Renommage AppL en AppGravatar herbelin2000-10-01
* Disparition du type oper mais nouveau type global_referenceGravatar herbelin2000-10-01
* Abstraction de constrGravatar herbelin2000-09-14
* Correction pour make docGravatar herbelin2000-09-10
* Suppression de AbstGravatar 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
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* Centralisation prod_name and co dans Environ; mkLambda_string dans TermGravatar herbelin2000-05-18
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* erreurs lexicales dans les patterns (manquait des espaces)Gravatar filliatr2000-03-30
* Ajout {prod,lambda}_nameGravatar herbelin2000-03-21
* TautoGravatar filliatr2000-03-20
* mauvais parenthesage dans hd_name (patterns imbriques)Gravatar filliatr2000-03-16
* Utilisation de l'env pour nommer les RelGravatar herbelin2000-03-16
* Abstraction de l'implémentation des signatures de Sign en vue intégration d...Gravatar herbelin2000-01-26
* gros commit de tout ce que j'ai fait pendant les vacances :Gravatar filliatr2000-01-21
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* Poursuite intégration du CasesGravatar herbelin1999-12-13
* modules profile, Coqinit et Coqtop (=main)Gravatar filliatr1999-12-03
* - environment -> safe_environmentGravatar filliatr1999-12-01
* - Typing -> Safe_typingGravatar filliatr1999-12-01
* Evd vient apres Environ -> id_of_existential expanseGravatar filliatr1999-11-26
* ajouts divers pour module PrinterGravatar filliatr1999-11-26
* typage des existentielles dans Typing_ev; suppression metamap inutiles dans t...Gravatar filliatr1999-11-25
* Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsGravatar filliatr1999-11-24
* les variables existentielles contiennent maintenant un environnement (typeGravatar filliatr1999-10-19
* - déplacement (encore une fois !) des variables existentielles : elles sontGravatar filliatr1999-10-18
* module LogicGravatar filliatr1999-10-14
* - re-introduction d'une evar_map dans unsafe_envGravatar filliatr1999-10-13
* deplacements des var. ex. hors du noyauGravatar filliatr1999-10-08