index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
command.ml
Commit message (
Expand
)
Author
Age
*
Remove some dead-code (thanks to ocaml warnings)
Pierre Letouzey
2014-03-05
*
Useless Evd.create_evar_defs.
Pierre-Marie Pédrot
2013-12-30
*
STM: capture type checking error (Closes: 3195)
Enrico Tassi
2013-12-24
*
Qed: feedback when type checking is done
Enrico Tassi
2013-12-24
*
Adding generic solvers to term holes. For now, no resolution mechanism nor
Pierre-Marie Pédrot
2013-11-27
*
Fixup bug 3145
pboutill
2013-11-03
*
Makes the new Proofview.tactic the basic type of Ltac.
aspiwack
2013-11-02
*
Future: better doc + restore ~pure optimization
gareuselesinge
2013-10-31
*
Conv_orable made functional and part of pre_env
gareuselesinge
2013-10-31
*
More monomorphic List.mem + List.assoc + ...
letouzey
2013-10-24
*
Turn many List.assoc into List.assoc_f
letouzey
2013-10-24
*
cList: set-as-list functions are now with an explicit comparison
letouzey
2013-10-23
*
declaration_hooks use Ephemeron
gareuselesinge
2013-10-18
*
Future: ported to Ephemeron + exception enhancing
gareuselesinge
2013-10-18
*
Removing a bunch of generic equalities.
ppedrot
2013-09-27
*
Removing almost all new_untyped_evar, and a bunch of Evd.add.
ppedrot
2013-09-18
*
get rid of closures in global/proof state
gareuselesinge
2013-08-08
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Use the Hook module here and there.
ppedrot
2013-05-12
*
Use definition_entry to declare local definitions
gareuselesinge
2013-05-09
*
A uniformization step around understand_* and interp_* functions.
herbelin
2013-05-09
*
Uniformization: isevars -> evdref/sigma/evd
herbelin
2013-05-09
*
Fixing r16487 on sharing evars between multiple parameters (missing List.rev).
herbelin
2013-05-09
*
Uniformizing the [if_warn] flag used for warning printing and put
ppedrot
2013-05-08
*
Declaration of multiple hypotheses or parameters now share typing
herbelin
2013-05-08
*
Share more information between constructors and arity of an inductive
herbelin
2013-05-08
*
Merging Context and Sign.
ppedrot
2013-04-29
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Fix bug# 2994, 2971 about better error messages.
msozeau
2013-03-22
*
Making local variable warning verbose by default.
ppedrot
2013-03-18
*
Modules and ppvernac, sequel of Enrico's commit 16261
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 13)
letouzey
2013-03-13
*
Allowing (Co)Fixpoint to be defined local and Let-style.
ppedrot
2013-03-11
*
Added a Local Definition vernacular command. This type of definition
ppedrot
2013-03-11
*
Uniformization of the "anomaly" command.
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
*
Implemented a full-fledged equality on [constr_expr]. By the way,
ppedrot
2012-12-14
*
Monomorphization (toplevel)
ppedrot
2012-11-26
*
Monomorphized a lot of equalities over OCaml integers, thanks to
ppedrot
2012-11-08
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
Cleaning interface of Util.
ppedrot
2012-09-18
*
Some documentation and cleaning of CList and Util interfaces.
ppedrot
2012-09-15
*
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
*
The new ocaml compiler (4.00) has a lot of very cool warnings,
regisgia
2012-09-14
*
Fix computation of obligations for mutually recursive definitions.
msozeau
2012-09-06
*
Assumption commands are now displayed as unsafe in Coqide.
aspiwack
2012-08-24
*
Updating headers.
herbelin
2012-08-08
*
Bug 2838: ExplApp in mutual inductive parameters
pboutill
2012-07-12
[next]