index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
library
Commit message (
Expand
)
Author
Age
...
|
*
|
|
|
Protect code against changes in Map interface.
Maxime Dénès
2016-01-06
*
|
|
|
|
Remove some unused functions.
Guillaume Melquiond
2016-01-02
*
|
|
|
|
Remove keys for evar and meta, since they cannot occur.
Guillaume Melquiond
2016-01-02
*
|
|
|
|
Remove some useless type declarations.
Guillaume Melquiond
2016-01-02
*
|
|
|
|
Remove Library.mem, which is pointless since 8.5.
Guillaume Melquiond
2015-12-31
*
|
|
|
|
Avoid a pointless conversion/copy.
Guillaume Melquiond
2015-12-22
*
|
|
|
|
Do not compose "str" and "to_string" whenever possible.
Guillaume Melquiond
2015-12-22
*
|
|
|
|
Move the From logic to Loadpath.expand_path.
Guillaume Melquiond
2015-12-22
*
|
|
|
|
Do not query module files that have already been loaded.
Guillaume Melquiond
2015-12-22
|
|
/
/
/
|
/
|
|
|
*
|
|
|
COMMENTS: added to some variants of "Globalnames.global_reference" type.
Matej Kosik
2015-12-18
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-08
|
\
|
|
|
*
|
|
|
Leveraging GADTs to provide a better Dyn API.
Pierre-Marie Pédrot
2015-12-05
*
|
|
|
Specializing the Dyn module to each usecase.
Pierre-Marie Pédrot
2015-12-04
|
*
|
|
Univs: fix bug #4443.
Matthieu Sozeau
2015-12-03
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-29
|
\
|
|
|
|
*
|
|
Univs: entirely disallow instantiation of polymorphic constants with
Matthieu Sozeau
2015-11-27
|
*
|
|
Avoid recording spurious Set <= Top.i constraints which are always
Matthieu Sozeau
2015-11-27
*
|
|
|
More efficient implementation of equality-up-to-universes in Universes.
Pierre-Marie Pédrot
2015-11-26
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-26
|
\
|
|
|
*
|
|
|
More invariants in UState.
Pierre-Marie Pédrot
2015-11-26
|
*
|
|
Univs: fix type_of_global_in_context not returning instantiated universe cont...
Matthieu Sozeau
2015-11-20
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-30
|
\
|
|
|
|
*
|
|
Add a way to get the right fix_exn in external vernacular commands
Matthieu Sozeau
2015-10-30
|
|
*
|
More uniformity in the style of comparison functions.
Arnaud Spiwack
2015-10-30
|
|
*
|
Make the code of compare functions linear in the number of constructors.
Arnaud Spiwack
2015-10-29
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-29
|
\
|
|
|
|
|
/
/
|
/
|
|
|
*
|
Univs: local names handling.
Matthieu Sozeau
2015-10-28
|
*
|
Avoid type checking private_constants (side_eff) again during Qed (#4357).
Enrico Tassi
2015-10-28
|
*
|
lib_stack: API to reorder the libstack
Enrico Tassi
2015-10-28
|
*
|
Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names
Matthieu Sozeau
2015-10-27
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-26
|
\
|
|
|
*
|
Declaremods: replace two anomalies by user errors (fix #3974 and #3975)
Pierre Letouzey
2015-10-25
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-15
|
\
|
|
|
*
|
Fix some typos.
Guillaume Melquiond
2015-10-13
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-09
|
\
|
|
|
*
|
Univs: fix bug #3807
Matthieu Sozeau
2015-10-08
|
*
|
Goptions: new value type: optional string
Enrico Tassi
2015-10-08
*
|
|
Splitting kernel universe code in two modules.
Pierre-Marie Pédrot
2015-10-06
|
/
/
*
|
Univs: Change intf of push_named_def to return the computed universe
Matthieu Sozeau
2015-10-02
*
|
Univs: refined handling of assumptions
Matthieu Sozeau
2015-10-02
*
|
Univs: fix minimization to allow lowering a universe to Set, not Prop.
Matthieu Sozeau
2015-10-02
*
|
Univs: fix Universe vernacular, fix bug #4287.
Matthieu Sozeau
2015-10-02
*
|
Univs: minimization, adapt to graph invariants.
Matthieu Sozeau
2015-10-02
*
|
Forcing i > Set for global universes (incomplete)
Matthieu Sozeau
2015-10-02
*
|
Universes: enforce Set <= i for all Type occurrences.
Matthieu Sozeau
2015-10-02
*
|
Unexport Loadpath.get_paths.
Guillaume Melquiond
2015-09-30
*
|
Fix dumb typo.
Guillaume Melquiond
2015-09-29
*
|
Make the interface of System.raw_extern_intern much saner.
Guillaume Melquiond
2015-09-29
*
|
Prevent States.intern_state and System.extern_intern from looking up files in...
Guillaume Melquiond
2015-09-29
*
|
Remove some uses of Loadpath.get_paths.
Guillaume Melquiond
2015-09-29
[prev]
[next]