index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
dev
/
top_printers.ml
Commit message (
Expand
)
Author
Age
*
Ajout affichage contexte local
herbelin
2004-03-15
*
prettyprint des constr_substituted + un wrapping de prglobal pour qu'il n'ech...
letouzey
2003-04-16
*
Globalisation tactiques
herbelin
2003-04-07
*
Options d'affichage maintenant dans Constrextern
herbelin
2003-04-07
*
Ajout affichage fconstr
herbelin
2002-12-05
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
ajout d'un printer pour les global_reference
letouzey
2002-11-04
*
Pretty-printing preliminaire des modules, commandes
coq
2002-08-19
*
Petites corrections ici et la
coq
2002-08-13
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Changé le nom du module Errors (errors.mli, errors.ml) en Cerrors parce
ddr
2002-02-20
*
suppression du retour chariot a la fin de print_pure_constr
barras
2002-02-07
*
compat ocaml 3.03
filliatr
2001-12-13
*
Suppression des local_constraints, des ctxtty et du focus.
clrenard
2001-11-06
*
GROS COMMIT:
barras
2001-11-05
*
Abstraction de l'immplementation de dirpath et implementation dans l'autre se...
herbelin
2001-10-17
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
Ajout du printer de tactiques + modif du Dynamic ocaml
delahaye
2001-09-30
*
Parsing
herbelin
2001-08-10
*
ajout d'un afficher de contexte et d'une fonction constbody_of_string
letouzey
2001-05-10
*
Changement de la structure des points fixes
barras
2001-05-03
*
entetes
filliatr
2001-03-15
*
module Explore générique et réécriture EAuto avec ce module; occur check ...
filliatr
2001-03-05
*
Déplacement de qualid dans Nametab, hors du noyau
herbelin
2001-03-01
*
Déplacement de qualid dans Nametab, hors du noyau
herbelin
2001-03-01
*
nouvelle implantation de la reduction
barras
2001-03-01
*
Printer
mohring
2000-12-15
*
Bug sur commit précédent
herbelin
2000-12-14
*
Enfin trouvé la cause d'exception; suppression de la capsule de rattrapage
herbelin
2000-12-14
*
Prise en compte qualid
herbelin
2000-11-26
*
Gros hack pour afficher les univers
herbelin
2000-11-11
*
suppression des (* open Generic *)
filliatr
2000-11-02
*
MAJ
herbelin
2000-10-23
*
MAJ
herbelin
2000-10-18
*
MAJ pr_uni
herbelin
2000-10-06
*
Renommage AppL en App
herbelin
2000-10-01
*
MAJ
herbelin
2000-10-01
*
MAJ
herbelin
2000-09-14
*
MAJ
herbelin
2000-09-12
*
Ajout d'un LetIn primitif.
herbelin
2000-09-10
*
Passage à des contextes de vars et de rels pouvant contenir des déclarations
herbelin
2000-07-24
*
Mise en place d'un choix constr/typed_type en remplacement de certains Cast
herbelin
2000-06-01
*
MAJ modifs Inductive
herbelin
2000-05-18
*
Ajout de PrintConstr pour debug
delahaye
2000-05-03
*
renommage de certains printers
herbelin
2000-05-03
*
Restructuration printer et parser
herbelin
2000-01-07
*
pretty-printers pour le debugger
filliatr
1999-12-14
*
Ajout pp pattern et rawterm
herbelin
1999-12-12
*
pour debugger dans le toplevel ocaml
filliatr
1999-12-03