index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
pptactic.mli
Commit message (
Expand
)
Author
Age
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
In "simpl c" and "change c with d", c can be a pattern.
herbelin
2009-12-24
*
Generic support for open terms in tactics
herbelin
2009-12-21
*
Made the interpretation levels rlevel/glevel/tlevel truly phantom
herbelin
2009-12-19
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
- Propagation des evars non résolues vers les with_bindings; permet par exemple
herbelin
2007-05-20
*
Ajout de la possibilité de faire référence dans certains cas à un nom
herbelin
2007-04-28
*
Suppression du type 'tac dans les abstract_argument_type: devenu inutile
herbelin
2006-11-20
*
Ajout option 'using lemmas' à auto/trivial/eauto
herbelin
2006-01-28
*
Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq
herbelin
2006-01-16
*
Remplacement Pp.qs par Pptactic.qsnew
herbelin
2005-12-28
*
Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...
herbelin
2005-12-26
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Correction printer des Tactic Notation
herbelin
2005-12-23
*
Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de tact...
herbelin
2005-12-21
*
Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...
herbelin
2005-05-17
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Nouvelle en-tête
herbelin
2004-07-16
*
Simplification afficheur de tactiques non primitive
herbelin
2003-09-18
*
Traduction des réferences arguments de commandes non primitives
herbelin
2003-09-09
*
Suppression définitive de lmatch et or_metanum dans tacinterp
herbelin
2003-05-21
*
Factorisation des produits de même type; parenthèses autour des x:=c et n:=...
herbelin
2003-04-29
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
*** empty log message ***
barras
2003-03-12
*
Debugger plus informatif
delahaye
2003-02-13
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29