index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
obligations.ml
Commit message (
Expand
)
Author
Age
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-05
|
\
|
*
Rename Ephemeron -> CEphemeron.
Maxime Dénès
2016-03-04
*
|
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-29
|
\
|
|
*
Implement support for universe binder lists in Instance and Program Fixpoint/...
Matthieu Sozeau
2016-01-23
*
|
merge
Matej Kosik
2016-01-11
|
\
\
|
*
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
*
|
|
Do not compose "str" and "to_string" whenever possible.
Guillaume Melquiond
2015-12-22
|
/
/
*
|
Moving three related small half-general half-ad-hoc utility functions
Hugo Herbelin
2015-12-05
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-03
|
\
|
|
*
Univs/Program: update the universe context with global universe
Matthieu Sozeau
2015-12-02
|
*
Fix bug #4444: Next Obligation performed after a Section opening was
Matthieu Sozeau
2015-12-02
*
|
Removing dead code in Obligations.
Pierre-Marie Pédrot
2015-12-02
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-29
|
\
|
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-26
|
\
|
|
*
Univs: carry on universe substitution when defining obligations of
Matthieu Sozeau
2015-11-24
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-20
|
\
|
|
*
Allow program hooks to see the refined universe_context at the end of a
Matthieu Sozeau
2015-11-19
*
|
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
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-29
|
\
|
|
*
Avoid type checking private_constants (side_eff) again during Qed (#4357).
Enrico Tassi
2015-10-28
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-10
|
\
|
|
*
Fix Next Obligation to not raise an anomaly in case of mutual
Matthieu Sozeau
2015-10-09
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-09
|
\
|
|
*
Univs: fix FingerTree contrib.
Matthieu Sozeau
2015-10-07
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-02
|
\
|
|
*
Univs/program: handle side effects in obligations.
Matthieu Sozeau
2015-10-02
|
*
Univs: fix many evar_map initializations and leaks.
Matthieu Sozeau
2015-10-02
*
|
Merge branch 'v8.5' into trunk
Maxime Dénès
2015-09-17
|
\
|
|
*
Univs: Add universe binding lists to definitions
Matthieu Sozeau
2015-09-14
*
|
All Program obligations now respect the Shrink Obligation flag.
Pierre-Marie Pédrot
2015-09-08
*
|
Fixing the Shrink Obligations option.
Pierre-Marie Pédrot
2015-09-08
|
/
*
Code cleaning in Obligations.
Pierre-Marie Pédrot
2015-08-22
*
obligations: wrap Ephemeron.get to make error more informative
Enrico Tassi
2015-06-23
*
Wrap the program_info type up in the ephemeron mechanism
Alec Faithfull
2015-06-23
*
Program: Do not reduce obligation types preemptively, only at
Matthieu Sozeau
2015-04-13
*
Add the possibility of defining opaque terms with program.
mlasson
2015-01-21
*
Getting rid of Exninfo hacks.
Pierre-Marie Pédrot
2014-12-16
*
Tentatively more informative report of failure when inferring
Hugo Herbelin
2014-12-11
*
Exporting the function handling side-effects only applied to terms.
Pierre-Marie Pédrot
2014-11-20
*
Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.
Arnaud Spiwack
2014-10-22
*
Splitting out of auto.ml a file hints.ml dedicated to hints so as to
Hugo Herbelin
2014-10-07
*
Merging some functions from evarutil.ml/evd.ml.
Hugo Herbelin
2014-09-29
*
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-12
*
Simplify even further the declaration of primitive projections,
Matthieu Sozeau
2014-08-30
*
Change the way primitive projections are declared to the kernel.
Matthieu Sozeau
2014-08-28
*
Fix program using an the unsubstituted type of the original obligation
Matthieu Sozeau
2014-08-14
*
- Fix bug introduced in obligations which wouldn't consider all evars that are
Matthieu Sozeau
2014-07-16
*
Better handling of the universe context in case of Admitted proof obligations.
Matthieu Sozeau
2014-07-10
[next]