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
...
|
*
Preservation of the name of evars/goals when applying pose/set/intro/clearbody.
Hugo Herbelin
2015-11-07
|
*
Tests for syntax "Show id" and [id]:tac (shelved or not).
Hugo Herbelin
2015-11-07
|
*
Fixing documention of Add Printing Coercion.
Hugo Herbelin
2015-11-07
*
|
Merge remote-tracking branch 'origin/v8.5' into upstream-trunk
Hugo Herbelin
2015-11-07
|
\
|
|
*
Fixed #4407.
Pierre Courtieu
2015-11-06
|
*
Fixing #4406 coqdep: No recursive search of ml (-I).
Pierre Courtieu
2015-11-06
|
*
Fixing complexity file f_equal.v.
Hugo Herbelin
2015-11-06
|
*
More on how to compile doc.
Hugo Herbelin
2015-11-06
|
*
Fixing complexity issue with f_equal. Thanks to J.-H. Jourdan
Hugo Herbelin
2015-11-06
|
*
Add test-suite file for #4273.
Matthieu Sozeau
2015-11-05
|
*
Fix bug #4273
Matthieu Sozeau
2015-11-05
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-05
|
\
|
|
*
Update version numbers and magic numbers for 8.5beta3 release.
Maxime Dénès
2015-11-05
|
*
Checker was forgetting to register global universes introduced by opaque
Matthieu Sozeau
2015-11-04
|
*
Univs: missing checks in evarsolve with candidates and missing a
Matthieu Sozeau
2015-11-04
|
*
Univs: update refman, better printers for universe contexts.
Matthieu Sozeau
2015-11-04
|
*
Hint Cut documentation and cleanup of printing (was duplicated and
Matthieu Sozeau
2015-11-04
|
*
Univs: compatibility with 8.4.
Matthieu Sozeau
2015-11-04
|
*
Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusion
Matthieu Sozeau
2015-11-04
|
*
Test file for #4397.
Maxime Dénès
2015-11-04
|
*
Update compatibility file for some of bug #4392
Jason Gross
2015-11-03
|
*
Fix bug #4397: refreshing types in abstract_generalize.
Matthieu Sozeau
2015-11-02
|
*
Fix bug #4151: discrepancy between exact and eexact/eassumption.
Matthieu Sozeau
2015-11-02
|
*
Refresh rigid universes as well, and in 8.4 compatibility mode,
Matthieu Sozeau
2015-11-02
|
*
Follow-up fix on Enrico's 6e376c8097d75b6e, with Enrico.
Maxime Dénès
2015-11-02
|
*
Adding syntax "Show id" to show goal named id (shelved or not).
Hugo Herbelin
2015-11-02
|
*
Made that the syntax [id]:tac also applies to the shelve, which is after all ...
Hugo Herbelin
2015-11-02
|
*
STM: fix undo into a branch containing side effects
Enrico Tassi
2015-11-02
|
*
STM: never reopen a branch containing side effects
Enrico Tassi
2015-11-02
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-30
|
\
|
|
*
Command.declare_definition: grab the fix_exn early (follows 77cf18e)
Enrico Tassi
2015-10-30
|
*
Manually expand red_tactic so that notations do not break reduction tactics. ...
Guillaume Melquiond
2015-10-30
|
*
Add a way to get the right fix_exn in external vernacular commands
Matthieu Sozeau
2015-10-30
|
*
Fix typo.
Guillaume Melquiond
2015-10-30
*
|
Monotonizing Tactics.change_arg.
Pierre-Marie Pédrot
2015-10-29
|
*
Handle side-effects of Vernacular commands inside proofs better, so that
Matthieu Sozeau
2015-10-29
|
*
Collect subproof universes in handle_side_effects.
Matthieu Sozeau
2015-10-29
*
|
Removing some goal unsafeness in Equality.
Pierre-Marie Pédrot
2015-10-29
*
|
Removing unused and useless exported function in Hints.
Pierre-Marie Pédrot
2015-10-29
*
|
Removing the evar_map argument from s_enter.
Pierre-Marie Pédrot
2015-10-29
*
|
Removing some goal unsafeness in inductive schemes.
Pierre-Marie Pédrot
2015-10-29
|
*
Manually expand the debugging versions of "trivial" and "auto". (Fix bug #4392)
Guillaume Melquiond
2015-10-29
|
*
Avoid an anomaly when destructing an unknown ident. (Fix bug #4395)
Guillaume Melquiond
2015-10-29
|
*
Fixing another instance of bug #3267 in eauto, this time in the
Hugo Herbelin
2015-10-29
|
*
Cleanup API and comments of 908dcd613
Enrico Tassi
2015-10-29
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-29
|
\
|
|
*
Accept option -compat 8.5. (Fix bug #4393)
Guillaume Melquiond
2015-10-29
|
*
Univs: local names handling.
Matthieu Sozeau
2015-10-28
|
*
Printing of @{} instances for polymorphic references in Print and About.
Matthieu Sozeau
2015-10-28
|
*
Avoid type checking private_constants (side_eff) again during Qed (#4357).
Enrico Tassi
2015-10-28
[prev]
[next]