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
...
*
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
*
Improving printing of 'rew' notation
herbelin
2013-05-05
*
Hack to solve a "Bad recursive type" anomaly.
herbelin
2013-05-05
*
Now printing body of abbreviations (i.e. notation with a name) with
herbelin
2013-05-05
*
Little fix for Nsatz: hypotheses not directly relevant to the nsatz
herbelin
2013-05-05
*
Improvement of r16204 on reporting tactic error locations: if the main
herbelin
2013-05-05
*
Relaxing the constraint on eta-expanding on the fly while looking for
herbelin
2013-05-05
*
Reporting the change on matching partial applications in patterns of
herbelin
2013-05-05
*
Removing a redundant function from Evd.
ppedrot
2013-05-03
*
Fix wrong computation of dependency signature in cases raising an uncaught ex...
msozeau
2013-04-30
*
Merging Context and Sign.
ppedrot
2013-04-29
[prev]
[next]