index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
Commit message (
Expand
)
Author
Age
*
Protection traducteur contre meta de Grammar tactic
herbelin
2003-09-09
*
Nouvelle mouture du traducteur v7->v8
herbelin
2003-08-11
*
switching back to old tauto
corbinea
2003-07-03
*
added hints into Ground
corbinea
2003-07-02
*
suppression de newtauto
corbinea
2003-07-02
*
*** empty log message ***
courant
2003-06-27
*
Une completion de l'interpretation des TacAlias pour la partie interpretable
herbelin
2003-06-25
*
Ground Update.
corbinea
2003-06-20
*
Ajout 'Symmetry in Hyp'
herbelin
2003-06-19
*
Ajout option Local à Hint, Hints et HintDestruct
herbelin
2003-06-14
*
Utilisation de intro_pattern dans NewDestruct/NewInduction
herbelin
2003-06-13
*
Ajout option translate_syntax pour caractériser l'interprétation du traduct...
herbelin
2003-06-12
*
Traducteur + passage des noms de tactiques à kernel_name pour compatibilité...
herbelin
2003-06-10
*
Ground and CCsolve updates
corbinea
2003-05-25
*
Amélioration affichage locations; prise en compte variables dans lettac; ajo...
herbelin
2003-05-24
*
Réparation d'un bug de backtracking qui lui-même succédait à une ineffica...
herbelin
2003-05-22
*
Preservation affichage des ?n en V7
herbelin
2003-05-22
*
Suppression définitive de lmatch et or_metanum dans tacinterp
herbelin
2003-05-21
*
Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...
herbelin
2003-05-21
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
Restructuration des procédures de filtrage
herbelin
2003-05-19
*
Separation entre les propositions de syntaxe - suite
herbelin
2003-05-13
*
Enhancement of the Ground tactic, addition of GTauto and GIntuition.
corbinea
2003-05-07
*
Localisation erreurs TacAlias; Globalisation moins tolérante dans les
herbelin
2003-04-28
*
Added the Ground tactic.
corbinea
2003-04-25
*
simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...
letouzey
2003-04-16
*
Localisation des appels de tactiques définies sans arguments
herbelin
2003-04-14
*
Bug: lookup inapproprie dans subst_tactic
herbelin
2003-04-14
*
Relachement globalisation Unfold en usage interactif
herbelin
2003-04-10
*
Trop de restriction pour les TacDef
herbelin
2003-04-10
*
Prise en compte des variables de grammaires de tactiques et dédollarisation ...
herbelin
2003-04-08
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
code mort
herbelin
2003-04-07
*
Backtrack du commit de Christine, qui posait probleme avec FTC
letouzey
2003-04-03
*
Extension de Replace aux égalités entre preuves
herbelin
2003-04-01
*
Ajout d'un message à FailTac
herbelin
2003-03-31
*
Ajout d'un message à FailTac; localisation des appels à des tactiques défi...
herbelin
2003-03-31
*
factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )
corbinea
2003-03-31
*
eq fusionne avec eqT et devient par défaut sur Type,
herbelin
2003-03-29
*
notations <>, Assumption avec existentiel, replace term
mohring
2003-03-28
*
Fixed Relative names not,iff in Camlp4 quotation.
corbinea
2003-03-28
*
Introducing Christine's Intuition1 and adding some invertible hyps.
corbinea
2003-03-18
*
*** empty log message ***
barras
2003-03-12
*
Changed Tauto so it displays less 'Unfold not iff'
corbinea
2003-02-26
*
Correction d'un bug introduit dans le backtracking d'occurrence
delahaye
2003-02-13
*
Chargement dynamique de .cma
delahaye
2003-02-13
*
Debugger plus informatif
delahaye
2003-02-13
*
Suppression de l'élimination des existentiels dans LinearIntuition.
corbinea
2003-02-05
*
Un type "standardisé" pour new_hyp
herbelin
2003-01-25
*
Ajout de LinearIntuition; Ajout de New(Tauto|Intuition|LinearIntuition).
corbinea
2003-01-23
[next]