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
*
Program: fix #4873: transparency option not used
Matthieu Sozeau
2016-07-07
*
rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...
Pierre Letouzey
2016-07-03
*
closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)
Pierre Letouzey
2016-07-03
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Program: refine shrinking of obligations
Matthieu Sozeau
2016-06-27
*
Rework treatment of default transparency of obligations
Matthieu Sozeau
2016-06-27
*
Shrink Proofs/Obligations by default and deprecate
Matthieu Sozeau
2016-06-27
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-27
|
\
*
|
Moving the typing_flags to the environment.
Pierre-Marie Pédrot
2016-06-18
*
|
Factorizing the uses of Declareops.safe_flags.
Pierre-Marie Pédrot
2016-06-16
*
|
Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.
Pierre-Marie Pédrot
2016-06-16
|
\
\
|
*
|
Allow `Pretyping.search_guard` to not check guard
Arnaud Spiwack
2016-06-15
*
|
|
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
|
|
*
Program: remove debug tracing
Matthieu Sozeau
2016-05-26
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-09
|
\
\
\
|
|
|
/
|
|
/
|
|
*
|
Fix bug #3887: Better error message for "More than one program with unsolved ...
Pierre-Marie Pédrot
2016-05-09
*
|
|
Moving the use of Tactic_option from Obligations to G_obligations.
Pierre-Marie Pédrot
2016-03-19
*
|
|
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
|
/
/
[next]