aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2005-03-08Ajout foldherbelin
2005-03-01Code mortherbelin
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ...herbelin
2005-02-18Standardisation of function names about global references (especially, renami...herbelin
2005-02-18Moving subst_inductive from tacinterp to inductiveops for better for reuse in...herbelin
2005-02-18Ajout it_mkNamedProd_wo_LetInherbelin
2005-02-18Ajout splay_lambdaherbelin
2005-02-12Uniformisation de destApplication en destAppherbelin
2005-02-12Ajout Print Canonical Structuresherbelin
2005-02-02Correction de la précédence des contexts de variables rel, ltac et varherbelin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2005-01-14Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedsacerdot
2005-01-03HUGE COMMITsacerdot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 15:57:29 +0000