aboutsummaryrefslogtreecommitdiff
path: root/pretyping/tacred.ml
AgeCommit message (Expand)Author
2009-02-19On remplace evar_map par evar_defs (seul evar_defs est désormais exporté aspiwack
2009-02-06pushed evar reduction in kernelbarras
2008-12-31Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->herbelin
2008-12-03improved simplbarras
2008-11-28another bug with simplbarras
2008-11-27fixed bug 1791: simpl was performing eta expansionbarras
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-06-10- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)herbelin
2008-05-21refined the conversion oraclebarras
2008-04-18Correction bug 1835 + correction bug occur-check résultant en unherbelin
2008-03-10fold travaille maintenant sur la forme beta-iota-zeta réduite duherbelin
2007-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
2007-09-21Petit complément au commit 10131.herbelin
2007-09-21- Fixing bug 1703 ("intros until n" falls back on the variable name whenherbelin
2007-05-21Protection d'un warning par if_verboseherbelin
2007-04-14Suite du commit 9760 : l'uniformisation du comportement de one_step_reduce,herbelin
2007-04-13Correction bug #1491herbelin
2007-04-13Nettoyage des tactiques basées sur "simpl" (delta-réduction cachantherbelin
2006-05-05amelioration de la machine interpretee (vecteurs au lieu de listes d'arguments)barras
2006-04-27Standardisation nom option_app en option_mapherbelin
2006-02-07Amélioration des messages d'erreurs de tacred; unfold considère maintenant leherbelin
2005-12-02Changement des named_contextgregoire
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par o...herbelin
2005-11-02Correction bug invert_names (cf bug #1031)herbelin
2005-05-20Adoption du nom canonique global_of_constr pour éviter confusion avec type r...herbelin
2005-02-12Uniformisation de destApplication en destAppherbelin
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-11-29UserError in reduce_to_*_refherbelin
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-08Un bug de simpl de 1995 + nettoyage (les args de list_fold_left_i etaient inc...herbelin
2004-09-03premiere reorganisation de l\'unificationbarras
2004-07-16Nouvelle en-têteherbelin
2004-06-29Essai de suppression de eta dans simpl (cf bug #779)herbelin
2004-04-30Terminologie plus intuitive: evaluable -> unfoldableherbelin
2004-04-07bug #606: mis un message d'erreur plus clairbarras
2004-02-13Bug numerotation des occurrences pour 'simpl id at n' (suite)herbelin
2004-02-13Bug numerotation des occurrences pour 'simpl id at n' (2 protections maintena...herbelin
2004-01-27Bug (destruct/induction ne savent pas traiter le cas non atomique avec paramÃ...herbelin
2003-12-23Affichage opaqueherbelin
2003-12-17Prise en compte des sous-termes imbriqués pour 'simpl ident at nums'herbelin
2003-11-22Bug introduit avec le 'Simpl f'herbelin
2003-11-21Ajout 'Simpl f'herbelin
2003-11-09Ajout reduce_to_quantified_refherbelin
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 17:50:16 +0000