index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
nbtermdn.ml
Commit message (
Expand
)
Author
Age
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
Partial revert of Yann commit in order to use CLib.List when opening
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
Noise for nothing
pboutill
2012-03-02
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Fix discrimination of sorts which doesn't play well with cumulativity
msozeau
2010-05-02
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Better use of transparency information for local hypotheses:
msozeau
2009-09-22
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Enhanced discrimination nets implementation, which can now work with
msozeau
2008-06-27
*
Factorisation des opérations sur le type option de Util dans un module
aspiwack
2007-12-05
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
The type Pattern.constr_label was isomorphic to Libnames.global_reference.
sacerdot
2004-12-07
*
Nouvelle en-tête
herbelin
2004-07-16
*
entetes
filliatr
2001-03-15
*
suppression des (* open Generic *)
filliatr
2000-11-02
*
Correction pour make doc
herbelin
2000-09-10
*
Ajout d'un LetIn primitif.
herbelin
2000-09-10
*
Déplacement du type reference dans Term
herbelin
2000-04-28
*
Introduction d'un type constr_pattern pour les différents filtrages
herbelin
2000-04-26
*
discriminations nets
filliatr
1999-11-19