aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term.ml
Commit message (Expand)AuthorAge
* Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de...Gravatar herbelin2001-09-19
* Suppression de Type_1, inutile, et non prévu dans le modèle des univers alg...Gravatar herbelin2001-09-09
* Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...Gravatar herbelin2001-07-21
* Ajout hashconsing universGravatar herbelin2001-07-03
* Facilites pour le debogguage des univers.Gravatar coq2001-05-29
* Ajout d'une fonction de remplacement d'un sous-terme par un terme.Gravatar clrenard2001-05-15
* Changement de la structure des points fixesGravatar barras2001-05-03
* interdiction occ positives ET negatives dans PatternGravatar werner2001-04-24
* Suppression de mk_constr qui ne respectait pas l'invariant des applications (...Gravatar herbelin2001-04-15
* entetesGravatar filliatr2001-03-15
* compare_constr independent du groupement des applications.Gravatar barras2001-03-08
* Re-Déplacement extended_rel_listGravatar herbelin2001-03-05
* nouvelle implantation de la reductionGravatar barras2001-03-01
* Changement de subst_metaGravatar mohring2001-02-28
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refGravatar herbelin2001-02-07
* Ajout global_vars_declGravatar herbelin2001-01-24
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Ajout map_constr_with_full_binders et strong pour SimplGravatar herbelin2000-11-27
* Reparation IsMutConstruct + TransparentGravatar mohring2000-11-23
* Introduction constant_path = section_pathGravatar herbelin2000-11-20
* Code mortGravatar herbelin2000-11-10
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Nouveau type rec_declarationGravatar herbelin2000-10-11
* Ajout let dans destArity, suppression de lift_context (lift_rel_context suffit)Gravatar herbelin2000-10-11
* correction bug univers (dummy_univ)Gravatar filliatr2000-10-06
* Rebranchement de la tactique LetGravatar herbelin2000-10-03
* Renommage AppL en AppGravatar herbelin2000-10-01
* Passage de la structure DOPN, DOP2, ... à une structure exprimant directemen...Gravatar herbelin2000-10-01
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* Suppression de AbstGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Pattern matching de sous-termesGravatar delahaye2000-08-17
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Ajout fonctions sur les aritésGravatar herbelin2000-07-01
* Ajout make_typed_lazyGravatar herbelin2000-06-29
* Retrait des lam_and_pop and co; ajout d'un destructeur 'lispien' de constrGravatar herbelin2000-06-03
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* Nettoyage de GenericGravatar herbelin2000-05-31
* Centralisation prod_name and co dans Environ; mkLambda_string dans TermGravatar herbelin2000-05-18
* Retrait de PrintConstr vers top_printersGravatar delahaye2000-05-03
* diverses modifs pour ocamlwebGravatar filliatr2000-05-03
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'Gravatar herbelin2000-05-02
* Déplacement du type reference dans TermGravatar herbelin2000-04-28
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
* Extension du case_info : ajout du nombre de vrais args de chaque constr pour ...Gravatar herbelin2000-03-21
* Ajout destApplicationGravatar herbelin2000-03-07
* MAJ ocaml 2.99 (espaces dans la syntaxe des cast)Gravatar herbelin2000-01-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 10:17:46 +0000