aboutsummaryrefslogtreecommitdiff
path: root/proofs/tacinterp.ml
AgeCommit message (Expand)Author
2002-05-29Déplacement de proofs vers tacticsherbelin
2002-05-27Ajout de Eval, Inst et Checkdelahaye
2002-05-15Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage deherbelin
2002-05-15Finalement VTactic est gardé pour y plonger les tactiques ML, leherbelin
2002-05-15Contournement de la fermeture ML dans VContextherbelin
2002-05-14- Changement de l'ordre de filtrage dans "Match Context"herbelin
2002-03-18Rétablissement de look_for_interpdelahaye
2002-03-17Meilleure gestion de la reduction dans Fielddelahaye
2002-03-12Retablissement de interp_tab + injection id -> constr sans goaldelahaye
2002-02-21code mort dans tactinterp; plus de Debug On/Off dans Correctnessfilliatr
2001-12-20Convertibilité au lieu d'alpha-équivalence pour les motifs non linéaires d...herbelin
2001-12-13compat ocaml 3.03filliatr
2001-11-29nouvel algo de conversion plus uniformebarras
2001-11-06Suite de la suppression : enamed_declaration est remplace par evar_map.clrenard
2001-11-05GROS COMMIT:barras
2001-10-23Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrRdelahaye
2001-10-17Abstraction de l'immplementation de dirpath et implementation dans l'autre se...herbelin
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-10-02Ajout de dynamiques pour les quotations constr et tacticdelahaye
2001-09-30Ajout du printer de tactiques + modif du Dynamic ocamldelahaye
2001-09-24Changement du message d'erreur pour l'interpreteur de tactiquesdelahaye
2001-09-21Correction due au changement de semantique de Matchdelahaye
2001-09-20Transparentbarras
2001-08-10Parsingherbelin
2001-07-19Changements dans le traitement des qualid'sdelahaye
2001-07-02Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans Compute...herbelin
2001-07-02Nettoyage/restructuration des ensembles d'indicateurs de réductionsherbelin
2001-06-29Backtracking pour le Matchdelahaye
2001-06-25Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...herbelin
2001-06-19Extension des parametres de Clear + Instdelahaye
2001-06-18Interpretation MetaId + Progress + Instdelahaye
2001-05-07quelques bug reports mineursbarras
2001-04-19Metas dans les Unfold'sdelahaye
2001-04-12Ajout de _ dans les patterns d'intromohring
2001-04-03utilisation de Options.if_verbosefilliatr
2001-03-28amelioration de la structure des universbarras
2001-03-15entetesfilliatr
2001-03-01Déplacement de qualid dans Nametab, hors du noyauherbelin
2001-02-16ident au lieu de string pour le nom de base de qualidherbelin
2001-02-07Reparation du pretty-print pour les tactiquesdelahaye
2001-02-06Correction pour les Unfold/Fold dans Cbvdelahaye
2001-01-31Mise en place de la possibilite d'unfolder des variables locales et des const...filliatr
2001-01-09Meta Definition + Tactic Definitiondelahaye
2001-01-05Arite cachee de Match Context + Meta Definitiondelahaye
2000-12-29Ajout du Let pour le langage de tactiquesdelahaye
2000-12-19Correction pour les variables abstraites dans les Tactic Definitionsdelahaye
2000-12-02Portage d'AutoRewritedelahaye
2000-11-28Elimination du 'delahaye
2000-11-27Ajout de evaluable_named_decl et evaluable_rel_decl en parallele au evaluable...herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:43:04 +0000