aboutsummaryrefslogtreecommitdiff
path: root/kernel/term.ml
AgeCommit message (Expand)Author
2000-05-18Centralisation prod_name and co dans Environ; mkLambda_string dans Termherbelin
2000-05-03Retrait de PrintConstr vers top_printersdelahaye
2000-05-03diverses modifs pour ocamlwebfilliatr
2000-05-03Ajout du langage de tactiquesdelahaye
2000-05-02Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'herbelin
2000-04-28Déplacement du type reference dans Termherbelin
2000-04-20Abstraction du type typed_type (un pas vers les jugements 2 niveaux)herbelin
2000-03-21Extension du case_info : ajout du nombre de vrais args de chaque constr pour ...herbelin
2000-03-07Ajout destApplicationherbelin
2000-01-26MAJ ocaml 2.99 (espaces dans la syntaxe des cast)herbelin
2000-01-26MAJ commentairesherbelin
2000-01-21gros commit de tout ce que j'ai fait pendant les vacances :filliatr
1999-12-15Nouveaux types 'constructor' et 'inductive' dans Term;herbelin
1999-12-11Intégration initiale du Casesherbelin
1999-12-10debug discharge et inductifsfilliatr
1999-12-09Ajout des messages d'erreurs de Casesherbelin
1999-12-01Intégration du Termast et du Retyping de HH, et modifications connexesherbelin
1999-12-01diverses fonctions ajouteesfilliatr
1999-11-27fin Recordops, et debut Evarutilfilliatr
1999-11-26ajouts divers pour module Printerfilliatr
1999-11-25Backtrack sur modif Evd.evd_conclherbelin
1999-11-24Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsfilliatr
1999-11-23modules Indrec, Tacentries, Hiddentacfilliatr
1999-10-20 - documentation repertoire proofs/filliatr
1999-10-14module Logicfilliatr
1999-10-13 - re-introduction d'une evar_map dans unsafe_envfilliatr
1999-10-08deplacements des var. ex. hors du noyaufilliatr
1999-09-07mise en place commandes minicoqfilliatr
1999-09-03 - environnements videsfilliatr
1999-08-30ajout des inductifs (sans types singletons pour l'instant)filliatr
1999-08-27suppression champs inutiles dans constantes et inductifs; verification defini...filliatr
1999-08-24mach et himsg; typage sans extractionfilliatr
1999-08-23 - suppression de CONV_X et CONV_X_LEQ : les univers sont maintenant toujoursfilliatr
1999-08-20machine: execute = typage avec universfilliatr
1999-08-19mise en place programmation literaire (generation de doc/coq.tex)filliatr
1999-08-18module Reduction (debut)filliatr
1999-08-17generic, term et evdfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 10:00:21 +0000