index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
library
/
libobject.ml
Age
Commit message (
Expand
)
Author
2009-10-06
Relaxed error severity when encountering unknown library objects or tactic
gmelquio
2009-09-17
Remove useless Liboject.export_function field
glondu
2009-09-17
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-08-06
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2008-12-29
- Added support for subterm matching in SearchAbout.
herbelin
2008-07-22
Correct implementation of discharging of implicit arguments and add new
msozeau
2008-04-02
Add the ability to specify the implicit status of section variables and
msozeau
2007-12-05
Factorisation des opérations sur le type option de Util dans un module
aspiwack
2007-01-10
Nouvelle approche pour le discharge modulaire
herbelin
2006-09-01
Indentation + typo
notin
2006-04-27
Standardisation nom option_app en option_map
herbelin
2005-02-18
Moving centralised discharge into dispatched discharge_function; required to ...
herbelin
2004-11-16
Names.substitution (and related functions) and Term.subst_mps moved to
sacerdot
2004-07-16
Nouvelle en-tête
herbelin
2002-08-02
Modules dans COQ\!\!\!\!
coq
2001-04-04
Added a flag that makes it possible to re-load files while taking only the
bertot
2001-03-15
entetes
filliatr
2000-11-15
methode export
filliatr
2000-05-31
Amélioration capture des erreurs
herbelin
1999-09-19
module Declare
filliatr
1999-09-18
module Library
filliatr
1999-09-03
modules Libobject et Summary (partiel)
filliatr
[prev]