aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2005-01-02Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...herbelin
2004-12-29ExtraRedExpr maintenant sans argument: pas très souple mais au moins convien...herbelin
2004-12-29Bug control_only_guardherbelin
2004-12-09Correction du bug de build_initial_predicate a révèlé un autre bug dans ex...herbelin
2004-12-09Achèvement correction bug do_restrict_hys: ne pas inverser les argumentsherbelin
2004-12-08Correction d'un bug historique de do_restrict_hyps + code mortherbelin
2004-12-08Correction d'un bug historique de do_restrict_hyps + code mortherbelin
2004-12-08Bugs dans la déclaration du type du terme filtré si non définiherbelin
2004-12-08Bug nom exceptionherbelin
2004-12-07The type Pattern.constr_label was isomorphic to Libnames.global_reference.sacerdot
2004-12-06Relâchement obligation d'une contrainte de type sur les Hole en position ter...herbelin
2004-12-06C'est trop compliqué de mettre à jour les types du metamap en passant sous ...herbelin
2004-12-06Commentaireherbelin
2004-12-03Propagation du nom des hyps du prédicat de filtrage pour le message d'erreur...herbelin
2004-11-29UserError in reduce_to_*_refherbelin
2004-11-26Correction bug #879herbelin
2004-11-26MAJ PCoFixherbelin
2004-11-19Fusion OBJDEF et OBJDEF1 et renommage en CANONICAL-STRUCTUIREherbelin
2004-11-16Names.substitution (and related functions) and Term.subst_mps moved tosacerdot
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
2004-11-12Changement dans les boxed values .gregoire
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-10-17Vérification de la typability de 'pattern'herbelin
2004-09-27?(mod_delta=true) parameter added to each unification function.sacerdot
2004-09-27collapse apps of patterns to avoid failuresbarras
2004-09-25Remplacement de l'exception NextOccurrence _ par PatternMatchingFailure dans ...herbelin
2004-09-23error if binder was already definedbarras
2004-09-17restructuration des printers: proofs passe avant parsingbarras
2004-09-15hiding the meta_map in evar_defsbarras
2004-09-12inclusion de meta_map dans evar_defsbarras
2004-09-10simplification de clenvbarras
2004-09-08unification encore...barras
2004-09-08petit bug avec les effets de bordsbarras
2004-09-08Un bug de simpl de 1995 + nettoyage (les args de list_fold_left_i etaient inc...herbelin
2004-09-07deuxieme vague de modifs: evar_defs fonctionnelbarras
2004-09-06mimick: unify types before making assignationbarras
2004-09-06bad env in mimick codebarras
2004-09-03deplacement de clenv vers pretypingbarras
2004-09-03premiere reorganisation de l\'unificationbarras
2004-08-24Expansion du prédicat du 'match' vis à vis de la dépendance en le terme fi...herbelin
2004-08-24Prise en compte expansion du prédicat du 'match' vis à vis de la dépendanc...herbelin
2004-08-24Ajout nom standard mkLambda_name pour lambda_name (et idem pour prod)herbelin
2004-08-24Deplacement des fonctions de typage des predicate de Cases a la V7 de inducti...herbelin
2004-08-23Correction bug #830 : les noms des implicites temporaires étaient inconnus a...herbelin
2004-07-16Nouvelle en-têteherbelin
2004-07-16Suppression de Rawterm.loc, branchement sur Util.locherbelin
2004-07-13bug #794: conv made in wrong envbarras
2004-07-13bug #790: better error_not_cleanbarras
2004-07-11Eta-expansion du predicat dans build_indrec (suite)herbelin
2004-07-11Eta-expansion du predicat pas seulement pour make_case mais aussi pour build_...herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 04:38:05 +0000