aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2000-05-22Rienherbelin
2000-05-22suppression de l'env/sigma dans les fonctions de reduction beta et iota seulsherbelin
2000-05-22Suite restructuration inductifs; changement nom module Constant en Declarationsherbelin
2000-05-18Effets de bords suite à la restructuration des inductives (cf Inductive)herbelin
2000-05-05Réorganisationherbelin
2000-05-04Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)herbelin
2000-05-03diverses modifs pour ocamlwebfilliatr
2000-05-03Ajout du langage de tactiquesdelahaye
2000-05-02pattern-matching non-exhaustif (occur_rawconstr)filliatr
2000-05-02Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'herbelin
2000-04-28Déplacement du type reference dans Termherbelin
2000-04-28Changement de représentation du contexte des réf dans rawconstr et patternherbelin
2000-04-27Retrait fullmind de inductive_summary pour simplicitéherbelin
2000-04-26renommage ancien pattern en cases_patternherbelin
2000-04-26N'importe quel rawconstr maintenant dans le contexte d'une référenceherbelin
2000-04-26Introduction d'un type constr_pattern pour les différents filtragesherbelin
2000-04-20Abstraction du type typed_type (un pas vers les jugements 2 niveaux)herbelin
2000-03-28Nettoyage de l'interface d'Astterm; renommage des constr_of_com and co en int...herbelin
2000-03-21Modification de type_of_case, type_case_branches, etcherbelin
2000-03-21Prise en compte nouveau case_infoherbelin
2000-03-21Plus besoin de env dans reduce_mind_caseherbelin
2000-03-21Inlining prod_createherbelin
2000-03-21Prise en compte nouveau case_infoherbelin
2000-03-21Extension du case_info : ajout du nombre de vrais args de chaque constr pour ...herbelin
2000-03-16Syntactic Definition n'etaient pas correctemenet importeesfilliatr
2000-03-16Qqes bugs (evars dans le predicat; tag des cas défauts)herbelin
2000-03-10*** empty log message ***barras
2000-03-10Reparation bug isevars dans pretypingherbelin
2000-03-08La partie 'val' de trad_constraints devient un typed_typeherbelin
2000-03-08MAJ nouveau try_mutind_ofherbelin
2000-03-08Un nouveau moteur pour Cases (phase 1)herbelin
2000-03-07Renommage mt_con -> empty_conherbelin
2000-03-07Commentaireherbelin
2000-03-07Export inh_conv_coerce_to et diversherbelin
2000-01-28documentationfilliatr
2000-01-27erreurs latex dans interfacesfilliatr
2000-01-26MAJ ocaml 2.99 (espaces dans la syntaxe des cast)herbelin
2000-01-26Abstraction de l'implémentation des signatures de Sign en vue intégration d...herbelin
2000-01-21gros commit de tout ce que j'ai fait pendant les vacances :filliatr
2000-01-20Broutillesherbelin
2000-01-13Plus d'unfold inutile des Fix dans Simplherbelin
2000-01-11Ajout de Recordherbelin
2000-01-07Traduction constr->rawconstr (avant dans Termastherbelin
2000-01-07Correction pbs liés aux evarherbelin
2000-01-07Déplacement non-affichage des coercions dans termastherbelin
1999-12-15Bug liftherbelin
1999-12-15Nouveaux types 'constructor' et 'inductive' dans Term;herbelin
1999-12-13 - états fabriqués avec -silentfilliatr
1999-12-13 - méthode load sur les Hintsfilliatr
1999-12-13Poursuite intégration du Casesherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 12:17:44 +0000