aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2002-07-17tactique Substfilliatr
2002-07-17Nettoyage de code pour la règle [id:(?1-> ?2)-> ?3|- ?]corbinea
2002-07-16Bug dans la globalisation des arguments de tactiques primitivesherbelin
2002-07-15Correction bug Tauto : la regle pour (A->B)->C echouait quand C etaitcourant
2002-07-11Que la localisation des erreurs pour les tactiques atomiques marcheherbelin
2002-07-03Hack pour autoriser les $n dans les Grammar tacticherbelin
2002-06-13Réparation de l'interprétation des fermetures (sans casser Field!)herbelin
2002-06-06Ajout coercion constr vers hyp quantifiéeherbelin
2002-06-06Tentative de réparation d'un bug Omega: une variable de section qui après e...herbelin
2002-06-06Passage de PatternMatchingFailure vers UserError pour capture par tclFIRSTherbelin
2002-06-05Repercussion de la possibilit de mettre des hyps quantifiees dans Simplify_eq...herbelin
2002-06-05Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq e...herbelin
2002-06-05Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...herbelin
2002-05-31Les VContext ne sont plus des fermetures (temporaire)delahaye
2002-05-30Nettoyageherbelin
2002-05-30Finalement un seul constr pour l'instant dans ExtraRedExprherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-05-29Fichiers tactics/*.ml4 remplacent les tactics/*.vherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-05-29Réorganisation des tclTHEN (cf dev/changements.txt)herbelin
2002-05-29Fichiers tactics/*.ml4 remplacent les tactics/*.vherbelin
2002-05-29Pour les tactiques dépendant de Falseherbelin
2002-05-22Correction of a bug in Intuition (no more decomposition of dependent pairs).corbinea
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-14- Changement de l'ordre de filtrage dans "Match Context"herbelin
2002-05-14ajout des theoremes eqT_rec_r et eqT_rect_r pour Rewritebarras
2002-05-14Changement de eq en eqT comme equivalence de setoide par defaut.clrenard
2002-05-02Minor correction of get_lem_namecoq
2002-05-02nettoyage codecourant
2002-04-11Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.mlherbelin
2002-04-08*** empty log message ***courant
2002-04-02- modifs de la condition de garde pour mieux tenir compte des raisonnementsbarras
2002-03-27Simplification de Proof_type.prim_ruleherbelin
2002-03-26Prise en compte des dependances dans la tactique Casemohring
2002-03-21Intuition ne fait plus de Unfold des constantes (il faut les fairecourant
2002-03-20Intuition now takes an (optional) tactic as parameter. This tactic iscourant
2002-03-15Tauto est maintenant stable par "Intro" :courant
2002-03-13*** empty log message ***mohring
2002-03-07Simplify_eq echouait sur des hypotheses trivial comme O=Obarras
2002-03-05*** empty log message ***barras
2002-03-05assert failure avec Conditional Rewritebarras
2002-03-05suppression de code mortbarras
2002-03-04Nouveau Rewrite-in plus economiquebarras
2002-03-01labels appliques dans un ordre incorrectbarras
2002-02-28Uniformisation convert_hyp; correction problème de dépendance dans letin_tacherbelin
2002-02-22suppression de pop_namedbarras
2002-02-19Elim dependente n'appelait pas la bonne fonction pour calculer le predicatbarras
2002-02-18but de CutRewrite <- (assert false)barras
2002-02-15petits changements cosmetiques sur les tactiquesbarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 06:24:07 +0000