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
...
*
Déplacement et export de locate_global (ex-locate_reference) de tacinterp ve...
herbelin
2005-05-20
*
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
*
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
*
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
*
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
*
Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...
herbelin
2004-12-06
*
Names.substitution (and related functions) and Term.subst_mps moved to
sacerdot
2004-11-16
*
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-11-16
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...
herbelin
2004-10-11
*
- Prise en compte de Fail n (n>0) dans plusieurs cas qui avaient
herbelin
2004-09-25
*
Nouvelle en-tête
herbelin
2004-07-16
*
Abstraction vis a vis de dummy_loc
herbelin
2004-07-16
*
moved instantiate binding to extratactics
corbinea
2004-06-29
*
more evar stuff
corbinea
2004-06-28
*
Ajout de la coercion id dans context vers evaluable constant (bug #777)
herbelin
2004-06-28
*
effective evar refining
corbinea
2004-06-26
*
Clarify the distinction between quantified_hypothesis and declared_or_quantif...
herbelin
2004-06-02
*
Terminologie plus intuitive: evaluable -> unfoldable
herbelin
2004-04-30
*
Correction bug internalisation 'context'
herbelin
2004-03-10
*
modif des fixpoints pour que si on donne une notation au produit, les pts fix...
barras
2004-03-05
*
Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...
herbelin
2004-03-02
*
Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...
herbelin
2004-03-02
*
Généralisation du type ltac Identifier en IntroPattern; prise en compte des...
herbelin
2004-03-01
*
added breakpoints to help ide
corbinea
2004-02-26
*
- fixed the Assert_failure error in kernel/modops
barras
2004-02-18
*
Typo
herbelin
2004-02-12
*
Plus d'explicitation d'un message d'erreur
herbelin
2004-02-12
*
Localisation des erreurs d'internalisation des notations de tactiques
herbelin
2004-02-12
*
bugs avec Pose et Assert
barras
2004-01-09
*
*** empty log message ***
barras
2003-12-23
*
modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes
barras
2003-12-15
*
Nouvelle tactique EExists
clrenard
2003-12-01
*
Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...
herbelin
2003-11-25
*
New tactics : econstructor, eleft, eright, esplit
clrenard
2003-11-17
*
factorisation et generalisation des clauses
barras
2003-11-13
*
Prise en compte des alias syntaxiques vers des references dans divers lieux d...
herbelin
2003-11-12
*
Idtac peut prendre un argument à afficher
narboux
2003-11-12
*
Traduction semantique des InHyp de clause en InHypValue si local def
herbelin
2003-11-09
*
Added Instantiate ... in
corbinea
2003-11-06
*
Amelioration message d'erreur avec pretyping; prise en compte syntactic def d...
herbelin
2003-11-04
[prev]
[next]