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
*
Debugging en syntaxe v8
herbelin
2006-02-05
*
Réorganisation de la structure interne des types de déclarations (decl_kinds)
herbelin
2006-01-28
*
Ajout option 'using lemmas' à auto/trivial/eauto
herbelin
2006-01-28
*
Suppression code pour hints nommés à la V7 (voire à la V6...)
herbelin
2006-01-28
*
Suppression de la dépendance en Map.fold de ocaml dont la sémantique a
herbelin
2006-01-24
*
Messages de idtac et fail peuvent maintenant être des listes de string, int ...
herbelin
2006-01-21
*
Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et f...
herbelin
2006-01-21
*
Backtrack commit précédent (incompatible avec le choix de prendre Idtac com...
herbelin
2006-01-21
*
Ajout de la contrainte de résoudre l'assertion dans 'assert by'
herbelin
2006-01-20
*
Conséquences supplémentaires de la fin du support v7
herbelin
2006-01-19
*
Export eassumption
herbelin
2006-01-19
*
Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq
herbelin
2006-01-16
*
Code redondant
herbelin
2006-01-16
*
- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses
herbelin
2006-01-16
*
Standardisation du nom de subst_raw en subst_rawconstr
herbelin
2006-01-11
*
Standardisation du nom de subst_raw en subst_rawconstr
herbelin
2006-01-11
*
Résidus du traducteur v7 -> v8
herbelin
2006-01-11
*
Restructuration et simplification des fonctions d'affichage, de détypage
herbelin
2006-01-11
*
Ajout paramétricité du nom de la base de hint dans auto et trivial
herbelin
2006-01-11
*
Nettoyage coqlib
herbelin
2005-12-30
*
Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...
herbelin
2005-12-26
*
Petite correction nom QuantHypArgType suite suppression traducteur
herbelin
2005-12-26
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Prise en compte de l'information que certaines tactiques attendent un type (u...
herbelin
2005-12-21
*
Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de tact...
herbelin
2005-12-21
*
Changement des named_context
gregoire
2005-12-02
*
A la demande de Julien Forest
letouzey
2005-11-17
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
Confusion message erreur détectée par nouveau warning X de ocaml 3.09
herbelin
2005-11-04
*
Types inductifs parametriques
mohring
2005-11-02
*
Petit bug Declare Implicit Tactic
herbelin
2005-09-10
*
Nouvelle déclaration 'Declare Implicit Tactic' pour automatiser la résoluti...
herbelin
2005-09-09
*
Réparation bug #1000 (attendre fin de toutes les intros avant d'effacer les ...
herbelin
2005-09-08
*
Réparation bug #1004; nettoyage
herbelin
2005-09-08
*
Sur le conseil de X.Leroy: x=[||] devient Array.length x=0
letouzey
2005-08-19
*
Correction double bug #986: Fold ne préserve pas nécessairement le typage e...
herbelin
2005-07-13
*
essai de typage des instantiations d\'evars
barras
2005-06-06
*
New commit to allow definitions of morphisms on relations whose carrier is
sacerdot
2005-05-24
*
New command: "Print Ltac qualid" to print user defined tactics.
sacerdot
2005-05-20
*
Adoption du nom canonique global_of_constr pour éviter confusion avec type r...
herbelin
2005-05-20
*
Déplacement et export de locate_global (ex-locate_reference) de tacinterp ve...
herbelin
2005-05-20
*
Setoid_replace: improved error message when trying to replace a term in a
sacerdot
2005-05-19
*
A wish by Bas Spitters granted: a little more of unification up to
sacerdot
2005-05-19
*
Implemented autorewrite with ... in hyp [using ...].
sacerdot
2005-05-18
*
Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...
herbelin
2005-05-17
*
Globalisation des Tactic Notation
herbelin
2005-05-15
*
Allow auto to have a parametric argument (wish #967)
herbelin
2005-05-15
*
Improved order of interpretation of atomic tactics (cf bug #952)
herbelin
2005-04-29
*
Ajout de l'axiome du but prouve par la tactique simplifi
coq
2005-03-22
*
Correction bug de dependent_hyps qui ne met pas à jour le type des hyps dép...
herbelin
2005-03-20
[next]