index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
tacinterp.ml
Commit message (
Expand
)
Author
Age
*
Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.
herbelin
2007-04-28
*
Extension to the general sequence operator (tactical). Now in addition to ...
emakarov
2007-04-02
*
Add a parameter to QuestionMark evar kind to say it can be turned into an obl...
msozeau
2007-03-19
*
Réparation absence d'interprétation des liaisons vers listes
herbelin
2007-02-15
*
Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de
herbelin
2007-02-13
*
Suppression de code mort
notin
2007-02-01
*
Changement dans le kernel :
bgregoir
2006-12-11
*
simplif de la partie ML de ring/field
barras
2006-10-27
*
Extension de la primitive ltac fresh pour qu'elle accepte une liste de
herbelin
2006-10-24
*
Interprétation du terme comme type dans 'change' si pas de 'with' (pour bén...
herbelin
2006-10-24
*
affichage des ... dans les scripts
barras
2006-10-16
*
mise a jour du nouveau ring et ajout du nouveau field, avant renommages
barras
2006-09-26
*
Permet a un unfold de recevoir ses occurences a travers une variable Ltac.
letouzey
2006-09-25
*
Correction bug #1229 (toplevel "unresolved evar" fled through
herbelin
2006-09-23
*
Ajout d'une valeur VList dans tacinterp pour permettre de cabler des
herbelin
2006-09-22
*
Indentation + svnprop
notin
2006-09-12
*
improve the amount of information given by the Ltac tactic debugger
bertot
2006-08-28
*
corrects an error in the substitution of module paths inside tactics:
bertot
2006-08-17
*
Backtrack sur l'introduction de contraintes sur l'absence des 'ident' dans l'...
herbelin
2006-06-27
*
Préservation compatibilité interprétation quantified hypothesis (provisoir...
herbelin
2006-06-23
*
Nettoyage, uniformisation
herbelin
2006-06-22
*
Harmonisation de l'interprétation des intropattern
herbelin
2006-06-21
*
bug serieux efficacite de ltac
barras
2006-06-19
*
Changement du type d'argument 'TacticArgType X' en un type
herbelin
2006-06-08
*
Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...
herbelin
2006-05-30
*
Extension syntaxique de rewrite in: au lieu de pouvoir faire
letouzey
2006-05-02
*
Standardisation du nom des méthodes de Evd
herbelin
2006-04-28
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
Made pretyping a functor over a coercion implementation. Pretyping.Default us...
msozeau
2006-03-22
*
+ destruct now works as induction on multiple arguments :
jforest
2006-03-21
*
Correction bug 984 via introduction TacCall(loc,r,[]) pour signifier une réf...
herbelin
2006-03-05
*
induction now admits multiple induction arguments. The principle must
coq
2006-02-10
*
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
*
Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et f...
herbelin
2006-01-21
*
Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq
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
*
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
*
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
*
Changement des named_context
gregoire
2005-12-02
*
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
*
Nouvelle déclaration 'Declare Implicit Tactic' pour automatiser la résoluti...
herbelin
2005-09-09
*
New command: "Print Ltac qualid" to print user defined tactics.
sacerdot
2005-05-20
[next]