index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
printer.ml
Commit message (
Expand
)
Author
Age
*
Integrate a few improvements on typeclasses and Program from the equations br...
msozeau
2009-10-28
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Simplifying the call to print_no_goals and not calling it when no goal
herbelin
2009-06-11
*
Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0
herbelin
2009-06-06
*
- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence
herbelin
2009-05-09
*
Optionally list opaque constants in addition to axions/variables in
msozeau
2009-03-09
*
- Added support for subterm matching in SearchAbout.
herbelin
2008-12-29
*
closed bug 1898: fold x in x; added a reordering primitive tactic
barras
2008-11-26
*
- Fixed bug 1968 (inversion failing due to a Not_found bug introduced in
herbelin
2008-11-09
*
duplicated open of Ppconstr
letouzey
2008-10-21
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
Uniformisation du format des messages d'erreur (commencent par une
herbelin
2008-07-17
*
Various bug fixes in type classes and subtac:
msozeau
2008-07-01
*
Correction du problème de complexité de Print Assumptions :
aspiwack
2008-05-27
*
- Add pretty-printers for Idpred, Cpred and transparent_state, used for
msozeau
2008-04-24
*
Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)
herbelin
2008-03-10
*
Nettoyage de code en vue de la release. Plus de Warning: Unused
aspiwack
2007-12-18
*
Print Assumptions est pret pour la release.
aspiwack
2007-12-17
*
Plus de combinateurs sont passés de Util à Option. Le module Options
aspiwack
2007-12-06
*
Affichage de "thesis" seulement en mode déclaratif
herbelin
2007-07-18
*
Factorisation des types dans l'affichage des paramètres des (Co)Inductif/Record
herbelin
2007-06-30
*
killing some more non-exhaustive patterns
letouzey
2007-06-26
*
Corrections dans le Print Assumption. Les definitions locales ("Let")
aspiwack
2007-05-30
*
- Propagation des evars non résolues vers les with_bindings; permet par exemple
herbelin
2007-05-20
*
Processor integers + Print assumption (see coqdev mailing list for the
aspiwack
2007-05-11
*
fin des conclusions multiples
corbinea
2007-04-26
*
decl mode: anonymous facts
corbinea
2007-01-25
*
Correction du bug #1315:
notin
2007-01-22
*
Merge from Lionel Elie Mamane's private branch:
lmamane
2007-01-10
*
The emacs-U option now does not output *any* char above 250.
courtieu
2006-11-17
*
Déplacement surround dans util.ml et parenthésage des déclarations
herbelin
2006-09-23
*
Declarative Proof Language: main commit
corbinea
2006-09-20
*
Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsort
herbelin
2006-05-19
*
Export de pr_lconstr_pattern, pr_lconstr_pattern_env et pr_lpattern_expr;
herbelin
2006-04-24
*
Compatibilité prterm
herbelin
2006-01-12
*
Suite réorganisation des fonctions d'affichage
herbelin
2006-01-11
*
Restructuration et simplification des fonctions d'affichage, de détypage
herbelin
2006-01-11
*
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
*
Changement des named_context
gregoire
2005-12-02
*
Add some debug printing functions.
coq
2005-07-15
*
Clarification des niveaux pr_constr et pr_lconstr en v8 dans pr_prim_rule (cu...
herbelin
2005-02-03
*
Mecanisme d'affichage des types (notamment les conclusions des buts) typiquem...
herbelin
2004-12-22
*
* added subst_evaluable_reference
sacerdot
2004-12-07
*
The type Pattern.constr_label was isomorphic to Libnames.global_reference.
sacerdot
2004-12-07
*
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-11-16
*
restructuration des printers: proofs passe avant parsing
barras
2004-09-17
*
deplacement de clenv vers pretyping
barras
2004-09-03
*
Nouvelle en-tête
herbelin
2004-07-16
*
Le printeur de Show Script n'etait pas le bon en v7
herbelin
2003-11-02
[next]