aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term.ml
Commit message (Expand)AuthorAge
* 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
* MAJ commentairesGravatar 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
* Intégration initiale du CasesGravatar herbelin1999-12-11
* debug discharge et inductifsGravatar filliatr1999-12-10
* Ajout des messages d'erreurs de CasesGravatar herbelin1999-12-09
* Intégration du Termast et du Retyping de HH, et modifications connexesGravatar herbelin1999-12-01
* diverses fonctions ajouteesGravatar filliatr1999-12-01
* fin Recordops, et debut EvarutilGravatar filliatr1999-11-27
* ajouts divers pour module PrinterGravatar filliatr1999-11-26
* Backtrack sur modif Evd.evd_conclGravatar herbelin1999-11-25
* Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsGravatar filliatr1999-11-24
* modules Indrec, Tacentries, HiddentacGravatar filliatr1999-11-23
* - documentation repertoire proofs/Gravatar filliatr1999-10-20
* 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
* mise en place commandes minicoqGravatar filliatr1999-09-07
* - environnements videsGravatar filliatr1999-09-03
* ajout des inductifs (sans types singletons pour l'instant)Gravatar filliatr1999-08-30
* suppression champs inutiles dans constantes et inductifs; verification defini...Gravatar filliatr1999-08-27
* mach et himsg; typage sans extractionGravatar filliatr1999-08-24
* - suppression de CONV_X et CONV_X_LEQ : les univers sont maintenant toujoursGravatar filliatr1999-08-23
* machine: execute = typage avec universGravatar filliatr1999-08-20
* mise en place programmation literaire (generation de doc/coq.tex)Gravatar filliatr1999-08-19
* module Reduction (debut)Gravatar filliatr1999-08-18
* generic, term et evdGravatar filliatr1999-08-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-17 22:57:27 +0000