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
*
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
*
Mauvais environnement d'évaluation pour les globaux
herbelin
2003-01-22
*
Correction bug réecriture à la racine pour le sétoide Prop.
clrenard
2003-01-22
*
Plus du tout de backtracking dans "Match term"; vrai Exit dans débogueur
herbelin
2003-01-21
*
Mauvaise interprétatin de IdentArgType
herbelin
2003-01-20
*
Protection contre les noms de tactiques inconnus; restriction exceptions ratt...
herbelin
2003-01-20
*
Petits bugs
herbelin
2003-01-20
*
Utilisation d'une exception 'catchable'
herbelin
2003-01-19
*
Restructuration interpréteur de tactique: plus d'évaluation partielle à la...
herbelin
2003-01-19
*
Restructuration interpréteur de tactique: plus d'évaluation partielle à la...
herbelin
2003-01-19
*
Subst sur une hyp qui n'existe pas ne fait pas une anomalie
barras
2003-01-16
*
correction de bug de Subst: ne faisait rien lorsque l'hypothese
barras
2003-01-09
*
Commentaires; optimisation
herbelin
2002-12-30
*
Utilisation du second-ordre avec possibilité de K-rédex dans lemInv
herbelin
2002-12-24
[next]