aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
2003-10-08Bug utilisation nametab pour ltacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4550 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-08Des abbreviations pour constrintern.ml; generic argument IdentArgherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4547 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Correction bug NewInduction pour les inductifs de type 'ordinaux'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4462 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Bug internalisation des Extern: la globalisation doit etre stricteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4453 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22Passage à la V8 par défautherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4437 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-18Interface Eautoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4415 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Indépendance vis à vis de Declareherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4372 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-11Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4352 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-09Protection traducteur contre meta de Grammar tacticherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4327 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
Option -v8 à coqtop lance coqtopnew Le terminateur reste "." en v8 Ajout construction primitive CLetTuple/RLetTuple Introduction typage dans le traducteur pour traduire les Case/Cases/Match Ajout mutables dans RCases or ROrderedCase pour permettre la traduction Ajout option -no-strict pour traduire les "Set Implicits" en implicites stricts + Bugs ou améliorations diverses Raffinement affichage projections de Record/Structure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4257 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-07-03switching back to old tautocorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4219 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-07-02added hints into Groundcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4215 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-07-02suppression de newtautocorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4214 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-27*** empty log message ***courant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4209 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-25Une completion de l'interpretation des TacAlias pour la partie interpretableherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4206 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-20Ground Update.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4188 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-19Ajout 'Symmetry in Hyp'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4185 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-14Ajout option Local à Hint, Hints et HintDestructherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4163 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13Utilisation de intro_pattern dans NewDestruct/NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4154 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-12Ajout option translate_syntax pour caractériser l'interprétation du ↵herbelin
traducteur à proprement parler git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4139 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Traducteur + passage des noms de tactiques à kernel_name pour ↵herbelin
compatibilité avec les foncteurs + réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur de tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4112 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-25Ground and CCsolve updatescorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4075 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-24Amélioration affichage locations; prise en compte variables dans lettac; ↵herbelin
ajout FreshId git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4073 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-22Réparation d'un bug de backtracking qui lui-même succédait à une ↵herbelin
inefficacité git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4063 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-22Preservation affichage des ?n en V7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4060 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4054 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ↵herbelin
les metavariables de patterns; fusion NoHypId et Hyp git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4043 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Restructuration des procédures de filtrageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4032 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-13Separation entre les propositions de syntaxe - suiteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4005 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-07Enhancement of the Ground tactic, addition of GTauto and GIntuition.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3991 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-28Localisation erreurs TacAlias; Globalisation moins tolérante dans lesherbelin
définitions de tactiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3968 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-25Added the Ground tactic.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3955 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-16simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = ↵letouzey
list_skipn n l git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3931 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-14Localisation des appels de tactiques définies sans argumentsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3922 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-14Bug: lookup inapproprie dans subst_tacticherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3921 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10Relachement globalisation Unfold en usage interactifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3907 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10Trop de restriction pour les TacDefherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3899 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-08Prise en compte des variables de grammaires de tactiques et dédollarisation ↵herbelin
des metaident git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3870 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
pour compatibilité avec les modules. Globalisation partielle des invocations de tactiques hors définitions (partielle car noms des Intros/Assert/Inversion/... non connus). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3857 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3854 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-03Backtrack du commit de Christine, qui posait probleme avec FTCletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3842 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-01Extension de Replace aux égalités entre preuvesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3833 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Ajout d'un message à FailTacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3825 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Ajout d'un message à FailTac; localisation des appels à des tactiques ↵herbelin
définies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3824 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3815 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-29eq fusionne avec eqT et devient par défaut sur Type,herbelin
idem pour ex et exT, ex2 et exT2, all et allT git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3812 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-28notations <>, Assumption avec existentiel, replace termmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3802 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-28Fixed Relative names not,iff in Camlp4 quotation.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3799 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-14 13:07:33 +0000