aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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
2002-02-14- Reforme de la gestion des args recursifs (via arbres reguliers)barras
2002-02-11substitution et pattern modulo letbarras
2002-02-08mauvais comportement de l'inversion vis-a-vis des letsbarras
2002-02-07petit nettoyage de kernel/inductivebarras
2002-02-01Ajout tactiques Rename et Pose; modifications pour Inversionherbelin
2002-01-31changement generation de schema d'elimination, False_rec est primitif, Constr...mohring
2002-01-25Remplacement cut_intro par true_cut_anon pour Inversionherbelin
2002-01-25Bug calcul de la signature incorrecte en présence de letinherbelin
2002-01-24Remplacement cut_intro par true_cut_anonherbelin
2002-01-24Bug calcul de la signature incorrecte en présence de letinherbelin
2002-01-24Bug dépendances en les corps des let-in oubliéesherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-16 13:08:07 +0000