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
*
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
*
Le type d'un Let est considéré comme 'user-provided' par le noyau et doit d...
herbelin
2005-03-19
*
Report depuis la V8.0pl2 de la correction d'un bug du traducteur
herbelin
2005-03-19
*
appel de Simplify depuis Coq
coq
2005-03-18
*
Fix bug #931: leave dependent evars as such for refine
herbelin
2005-03-08
*
Added 'clear - id' to clear all hypotheses except the ones dependent in the s...
herbelin
2005-03-07
*
Moving subst_inductive from tacinterp to inductiveops for better for reuse in...
herbelin
2005-02-18
*
Standardisation of function names about global references (especially, renami...
herbelin
2005-02-18
*
Moving subst_inductive from tacinterp to inductiveops for better for reuse in...
herbelin
2005-02-18
*
Ajout constructeur External pour appel outil externe à Coq
herbelin
2005-02-04
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Bug (reported by Lionel Mamane) fixed: the test for non-occurrence of the
sacerdot
2005-01-18
*
Bug fixed (reported by Roland): the setoire_rewrite in tactic did not work
sacerdot
2005-01-17
*
HUGE COMMIT
sacerdot
2005-01-03
*
Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...
herbelin
2005-01-02
*
ExtraRedExpr maintenant sans argument: pas très souple mais au moins convien...
herbelin
2004-12-29
*
Restauration type casted_open_constr pour tactique refine car l'unification n...
herbelin
2004-12-09
*
* added subst_evaluable_reference
sacerdot
2004-12-07
*
The type Pattern.constr_label was isomorphic to Libnames.global_reference.
sacerdot
2004-12-07
*
Uniformisation du nom d'entrée openconstr en le nom du type open_constr
herbelin
2004-12-06
*
Garder les cast semble décidément le meilleur moyen de rester synchrone ave...
herbelin
2004-12-06
*
Suppression des cast après avoir utiliser l'information de type (Tacinv envo...
herbelin
2004-12-06
*
Déplacement de la coercion vis à vis du but au niveau de Refine
herbelin
2004-12-06
[next]