aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typing.ml
Commit message (Expand)AuthorAge
* Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedGravatar sacerdot2005-01-14
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* test de conversion laissait echapper exception NotConvertibleGravatar barras2004-05-14
* CommentairesGravatar herbelin2002-12-10
* Essai suppression nf_betaiota dans type_ofGravatar herbelin2002-12-09
* petite erreur dans le typage des let-inGravatar barras2002-03-28
* typage du produit: type_judgment appele avec contexte incorrectGravatar barras2002-02-19
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
* Rétablissement de la persistance des Cast; typage des LetIn sans recours à ...Gravatar herbelin2001-11-08
* GROS COMMIT:Gravatar barras2001-11-05
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
* Changement de la structure des points fixesGravatar barras2001-05-03
* entetesGravatar filliatr2001-03-15
* nouvelle implantation de la reductionGravatar barras2001-03-01
* Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refGravatar herbelin2001-02-07
* Déplacement du message d'erreur de gen_rel vers l'appelant pour le prétypageGravatar herbelin2000-11-29
* 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
* Renommage AppL en AppGravatar herbelin2000-10-01
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* 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
* BricolesGravatar herbelin2000-06-29
* Rattrapage d'un Not_found pour les VAR's.Gravatar delahaye2000-06-28
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* Nettoyage de GenericGravatar herbelin2000-05-31
* Prise en compte nouveau case_infoGravatar herbelin2000-03-21
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* Intégration initiale du CasesGravatar herbelin1999-12-11
* Intégration du Termast et du Retyping de HH, et modifications connexesGravatar herbelin1999-12-01
* mise au point Declare et avancee dans AsttermGravatar filliatr1999-12-01
* - Typing -> Safe_typingGravatar filliatr1999-12-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 13:38:03 +0000