aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term.mli
Commit message (Expand)AuthorAge
* Nouvelle en-têteGravatar herbelin2004-07-16
* *** empty log message ***Gravatar barras2003-11-27
* CC: added injection theoryGravatar corbinea2003-11-25
* *** empty log message ***Gravatar courant2003-06-27
* Simplification case_infoGravatar herbelin2003-06-10
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Allègement du noyauGravatar herbelin2002-11-18
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Nouveau Rewrite-in plus economiqueGravatar barras2002-03-04
* substitution et pattern modulo letGravatar barras2002-02-11
* Ajout isEvarGravatar herbelin2001-11-20
* Ajout quelques fonctions; code mortGravatar herbelin2001-11-20
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
* GROS COMMIT:Gravatar barras2001-11-05
* Abstraction de l'immplementation de dirpath et implementation dans l'autre se...Gravatar herbelin2001-10-17
* Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...Gravatar herbelin2001-10-12
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de...Gravatar herbelin2001-09-19
* Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...Gravatar herbelin2001-09-10
* Suppression de Type_1, inutile, et non prévu dans le modèle des univers alg...Gravatar herbelin2001-09-09
* Comentaire errone.Gravatar clrenard2001-07-23
* Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...Gravatar herbelin2001-07-21
* Ajout hashconsing universGravatar herbelin2001-07-03
* 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
* Suppression de mk_constr qui ne respectait pas l'invariant des applications (...Gravatar herbelin2001-04-15
* mise a jour pour ocamlwebGravatar filliatr2001-04-02
* entetesGravatar filliatr2001-03-15
* Re-Déplacement extended_rel_listGravatar herbelin2001-03-05
* 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
* 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
* Introduction constant_path = section_pathGravatar herbelin2000-11-20
* Modification de la table des tactic Definitions pour eviter l'ecritureGravatar mohring2000-11-07
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* un espaceGravatar herbelin2000-10-24
* 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
* 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
* Abstraction de constrGravatar herbelin2000-09-14
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-02 12:20:09 +0000