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
...
*
|
|
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
*
|
Make -load-vernac-object respect the loadpath.
Guillaume Melquiond
2015-09-28
|
*
Show assumptions of well-foundedness in `Print Assumptions`
Arnaud Spiwack
2015-09-25
*
|
The -require option now accepts a logical path instead of a physical one.
Pierre-Marie Pédrot
2015-09-25
*
|
The -compile option now accepts ".v" files and outputs a warning otherwise.
Pierre-Marie Pédrot
2015-09-25
|
*
Propagate `Guarded` flag from syntax to kernel.
Arnaud Spiwack
2015-09-25
*
|
Hopefully better names to constructors of internal_flag, as discussed
Hugo Herbelin
2015-09-23
*
|
Nametab: print debug notice only in debug mode.
Maxime Dénès
2015-09-20
*
|
Add an if_verbose for "Fetching opaque proofs ..."
mlasson
2015-09-03
*
|
Fixing anomaly #3743 while printing an error message involving evar constraints.
Hugo Herbelin
2015-07-16
*
|
Option -type-in-type: added support in checker and making it contaminating
Hugo Herbelin
2015-07-10
*
|
Native compiler: refactor code handling pre-computed values.
Maxime Dénès
2015-07-10
*
|
Improve semantics of -native-compiler flag.
Maxime Dénès
2015-07-09
*
|
Univs/minimization: Fix unused variable bug.
Matthieu Sozeau
2015-07-07
*
|
Assumptions: more informative print for False axiom (Close: #4054)
Enrico Tassi
2015-06-29
*
|
Fix bug #4254 with the help of J.H. Jourdan
Matthieu Sozeau
2015-06-26
*
|
Wrapped the declare_object function to pretty-print anomalies at loading time.
Thomas Sibut-Pinote
2015-06-25
|
*
Make inductives that were assumed positive appear in `Print Assumptions`.
Arnaud Spiwack
2015-06-24
|
*
Add a corresponding field in `mutual_inductive_entry` (part 1).
Arnaud Spiwack
2015-06-24
|
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-06-24
|
|
\
|
|
/
|
/
|
*
|
On-demand Require.
Pierre-Marie Pédrot
2015-06-24
*
|
Splitting the library representation on disk in two.
Pierre-Marie Pédrot
2015-06-24
|
*
Wrapped the declare_object function to pretty-print anomalies at loading time.
Thomas Sibut-Pinote
2015-06-23
|
/
*
Fix bug #3446.
Matthieu Sozeau
2015-06-11
*
Fix bug #4159
Matthieu Sozeau
2015-05-27
*
Disable precompilation for native_compute by default.
Guillaume Melquiond
2015-05-14
*
Remove almost all the uses of string concatenation when building error messages.
Guillaume Melquiond
2015-04-23
*
Tactical `progress` compares term up to potentially equalisable universes.
Arnaud Spiwack
2015-04-22
*
Extra fix to 934761875 and f4ee7ee31e4 on optimizing Import of several
Hugo Herbelin
2015-04-17
*
Strengthen minimization: it shouldn't set a universe u to a max if it
Matthieu Sozeau
2015-04-09
*
Make it possible for -R to override the existing implicit setting of a path.
Guillaume Melquiond
2015-04-02
*
From X Require Y looks for X with absolute path, disregarding -R.
Pierre-Marie Pédrot
2015-04-01
*
Removing a probably incorrect on-the-fly require in a tactic.
Pierre-Marie Pédrot
2015-04-01
[prev]
[next]