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
...
*
Turn many List.assoc into List.assoc_f
letouzey
2013-10-24
*
cList.index is now cList.index_f, same for index0
letouzey
2013-10-23
*
declaration_hooks use Ephemeron
gareuselesinge
2013-10-18
*
Removing a bunch of generic equalities.
ppedrot
2013-09-27
*
At least made the evar type opaque! There are still 5 remaining unsafe
ppedrot
2013-09-18
*
Removing almost all new_untyped_evar, and a bunch of Evd.add.
ppedrot
2013-09-18
*
Partly replacing list-based access functions in Evd. This is still
ppedrot
2013-09-03
*
Added a more efficient way to recover the domain of a map.
ppedrot
2013-08-25
*
Less "Coq" strings everywhere
letouzey
2013-08-22
*
get rid of closures in global/proof state
gareuselesinge
2013-08-08
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Add an option to shrink the context of program obligations to avoid
msozeau
2013-06-06
*
Getting rid of LtacLocated exception transformer.
ppedrot
2013-05-28
*
Merging Context and Sign.
ppedrot
2013-04-29
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
code simplifications concerning Summary
letouzey
2013-04-22
*
Backport r16394 from 8.4:
msozeau
2013-04-11
*
Minor code cleaning in CArray / CList.
ppedrot
2013-03-23
*
Typo dans message d'erreur (obligations).
herbelin
2013-03-21
*
Restrict (try...with...) to avoid catching critical exn (part 13)
letouzey
2013-03-13
*
invalid_arg instead of raise (Invalid_argement ...)
letouzey
2013-03-12
*
Allowing different types of, not to be mixed, generic Stores through
ppedrot
2013-03-12
*
Allowing (Co)Fixpoint to be defined local and Let-style.
ppedrot
2013-03-11
*
Obligations generated by Program are now local.
ppedrot
2013-03-11
*
Added a Local Definition vernacular command. This type of definition
ppedrot
2013-03-11
*
Removing Exc_located and using the new exception enrichement
ppedrot
2013-02-18
*
Revised the Ltac trace mechanism so that trace breaking due to
herbelin
2013-02-17
*
Actually adding backtrace handling.
ppedrot
2013-01-28
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Added backtrace information to anomalies
ppedrot
2013-01-28
*
New implementation of the conversion test, using normalization by evaluation to
mdenes
2013-01-22
*
Modulification of identifier
ppedrot
2012-12-14
*
Moved Intset and Intmap to Int namespace.
ppedrot
2012-12-14
*
Monomorphization (toplevel)
ppedrot
2012-11-26
*
Monomorphized a lot of equalities over OCaml integers, thanks to
ppedrot
2012-11-08
*
Removed many calls to OCaml generic equality. This was done by
ppedrot
2012-10-29
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
More cleaning in CArray...
ppedrot
2012-09-18
*
As r15801: putting everything from Util.array_* to CArray.*.
ppedrot
2012-09-14
*
Partial revert of Yann commit in order to use CLib.List when opening
ppedrot
2012-09-14
*
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
Fixed #2893.
ppedrot
2012-09-10
*
Rationalized the behaviour of "Next Obligation" and "Admit Obligations"
ppedrot
2012-09-05
*
Cleaning opening of the standard List module.
ppedrot
2012-06-28
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
Separated notice vs info messages, and cleaned up the interface a bit.
ppedrot
2012-06-04
*
Cleaning Pp.ppnl use
ppedrot
2012-06-01
*
Getting rid of Pp.msgnl and Pp.message.
ppedrot
2012-06-01
*
Getting rid of Pp.msg
ppedrot
2012-05-30
[prev]
[next]