index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Delayed the computation of parameters in sort polymorphism of
herbelin
2013-05-14
*
"change ... in ..." and "simpl ... in ..." now consider nested
herbelin
2013-05-14
*
Fixing a regression in unification introduced in r16205 (error raised
herbelin
2013-05-14
*
Gmap is now useless, hail to Map!
ppedrot
2013-05-14
*
Removing the use of Gmap from Auto.
ppedrot
2013-05-14
*
Removing Gmap from Classops. Fold order only mattered for printing.
ppedrot
2013-05-14
*
Removing useless uses of Gmap.
ppedrot
2013-05-14
*
Removing Fmap from libraries, it is not used anymore.
ppedrot
2013-05-14
*
Replacing compatibility layer for Fmap in Typeclasses. Code was
ppedrot
2013-05-14
*
More semantical-friendly function.
ppedrot
2013-05-14
*
Replacing Id.check with Id.is_valid, as its sole use was under
ppedrot
2013-05-14
*
Removing Fset, since it is not used anymore.
ppedrot
2013-05-12
*
Removing the use of Fset/Fmap from Trie. There was actually only
ppedrot
2013-05-12
*
Documenting the previous commit.
ppedrot
2013-05-12
*
Granting wish #3014:
ppedrot
2013-05-12
*
Removing Gmap from Extraction plugin
ppedrot
2013-05-12
*
Use the Hook module here and there.
ppedrot
2013-05-12
*
Added a generic notion of hook. Hooks are functions to be set
ppedrot
2013-05-12
*
Fixing a source of evars leak, revealed by contrib QuicksortComplexity
herbelin
2013-05-11
*
Removing Gmap from Tacinterp.
ppedrot
2013-05-10
*
Little oversight in commit r16489 (fix for bug #3036).
herbelin
2013-05-10
*
Documenting the Tries module, uniformizing the names according to
ppedrot
2013-05-09
*
Updating some output tests in test-suite:
herbelin
2013-05-09
*
Use definition_entry to declare local definitions
gareuselesinge
2013-05-09
*
Cosmetic change
gareuselesinge
2013-05-09
*
Getting rid of module Gmapl.
ppedrot
2013-05-09
*
A uniformization step around understand_* and interp_* functions.
herbelin
2013-05-09
*
A few comments in evarconv.mli.
herbelin
2013-05-09
*
Uniformization: isevars -> evdref/sigma/evd
herbelin
2013-05-09
*
Fixing r16487 on sharing evars between multiple parameters (missing List.rev).
herbelin
2013-05-09
*
Removing unused module Nbtermdn.
ppedrot
2013-05-09
*
Removing Gmap from Notations.
ppedrot
2013-05-09
*
Xml_datatype.mli ships the xml type
gareuselesinge
2013-05-09
*
add Loadpath to printers.mllib
gareuselesinge
2013-05-09
*
Uniformizing the [if_warn] flag used for warning printing and put
ppedrot
2013-05-08
*
Protection against "Bad recursive type" in w_unify0 (bug #3036).
herbelin
2013-05-08
*
Alert when using ".." outside a Notation command.
herbelin
2013-05-08
*
Declaration of multiple hypotheses or parameters now share typing
herbelin
2013-05-08
*
Share more information between constructors and arity of an inductive
herbelin
2013-05-08
*
Moved isolated test params_ind.v to Inductive.v.
herbelin
2013-05-08
*
Fixing ocamldoc compilation.
ppedrot
2013-05-06
*
Small cleaning of Evd interface.
ppedrot
2013-05-06
*
fake_ide: xml parser does not check for EOF
gareuselesinge
2013-05-06
*
New module Xml_printer (dual to Xml_parser)
gareuselesinge
2013-05-06
*
Coqide: view -> zoom in / out / fit
gareuselesinge
2013-05-06
*
States: frozen states can hold closures
gareuselesinge
2013-05-06
*
Summary: support selective freeze
gareuselesinge
2013-05-06
*
Ideutils: comment on missing Glib utf8 handling function
gareuselesinge
2013-05-06
*
Close the .glob file after having saved .vo
gareuselesinge
2013-05-06
*
Fix typo in manual
gareuselesinge
2013-05-06
[next]