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
*
Fix handling of anonymous Type in template universe polymorphic inductives
Matthieu Sozeau
2014-06-04
*
- Fix treatment of global universe constraints which should be passed along
Matthieu Sozeau
2014-05-06
*
Proper calculation of constructor levels, forgetting the level of lets.
Matthieu Sozeau
2014-05-06
*
Retype application of fix_proto to get the right universes in Program
Matthieu Sozeau
2014-05-06
*
Fix restrict_universe_context removing some universes that do appear in the t...
Matthieu Sozeau
2014-05-06
*
Fix declarations of monomorphic assumptions
Matthieu Sozeau
2014-05-06
*
Fix program Fixpoint not taking care of universes.
Matthieu Sozeau
2014-05-06
*
- Fix bug preventing apply from unfolding Fixpoints.
Matthieu Sozeau
2014-05-06
*
Adapt Y. Bertot's path on private inductives (now the keyword is "Private").
Yves Bertot
2014-05-06
*
Correct rebase on STM code. Thanks to E. Tassi for help on dealing with
Matthieu Sozeau
2014-05-06
*
Rework handling of universes on top of the STM, allowing for delayed
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Removing Autoinstance once and for all.
Pierre-Marie Pédrot
2014-04-25
*
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
[next]