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
*
Univs: correctly register universe binders for lemmas.
Matthieu Sozeau
2015-11-28
*
Allow program hooks to see the refined universe_context at the end of a
Matthieu Sozeau
2015-11-19
*
Command.declare_definition: grab the fix_exn early (follows 77cf18e)
Enrico Tassi
2015-10-30
*
Univs: local names handling.
Matthieu Sozeau
2015-10-28
*
Avoid type checking private_constants (side_eff) again during Qed (#4357).
Enrico Tassi
2015-10-28
*
Univs: fix bug #4375, accept universe binders on (co)-fixpoints
Matthieu Sozeau
2015-10-28
*
Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names
Matthieu Sozeau
2015-10-27
*
Fix Definition id := Eval <redexpr> in by passing the right universe
Matthieu Sozeau
2015-10-12
*
Axioms now support the universe binding syntax.
Pierre-Marie Pédrot
2015-10-08
*
Univs: add Strict Universe Declaration option (on by default)
Matthieu Sozeau
2015-10-07
*
Univs: fix many evar_map initializations and leaks.
Matthieu Sozeau
2015-10-02
*
Universes: enforce Set <= i for all Type occurrences.
Matthieu Sozeau
2015-10-02
*
Univs: Add universe binding lists to definitions
Matthieu Sozeau
2015-09-14
*
Option -type-in-type: added support in checker and making it contaminating
Hugo Herbelin
2015-07-10
*
Fix bug #4254 with the help of J.H. Jourdan
Matthieu Sozeau
2015-06-26
*
Fix bug #4159
Matthieu Sozeau
2015-05-27
*
Safer typing primitives.
Pierre-Marie Pédrot
2015-05-13
*
Fixing computation of implicit arguments by position in fixpoints (#4217).
Hugo Herbelin
2015-05-01
*
Remove almost all the uses of string concatenation when building error messages.
Guillaume Melquiond
2015-04-23
*
Fixing #4017, #3726 (use of implicit arguments was lost in multiple variable ...
Hugo Herbelin
2015-02-10
*
Add the possibility of defining opaque terms with program.
mlasson
2015-01-21
*
Update headers.
Maxime Dénès
2015-01-12
*
kernel/ind Change interface of declare_mind and declare_mutual
Matthieu Sozeau
2015-01-05
*
Pass around information on the use of template polymorphism for
Matthieu Sozeau
2014-11-23
*
This commit introduces changes in induction and destruct.
Hugo Herbelin
2014-10-25
*
Change reduction_of_red_expr to return an e_reduction_function returning
Matthieu Sozeau
2014-10-24
*
Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.
Arnaud Spiwack
2014-10-22
*
Fixing #3193 (honoring implicit arguments in local definitions).
Hugo Herbelin
2014-10-03
*
Add syntax for naming new goals in refine: writing ?[id] instead of _
Hugo Herbelin
2014-09-30
*
Providing a -type-in-type option for collapsing the universe hierarchy.
Hugo Herbelin
2014-09-13
*
Uniformisation of the order of arguments env and sigma.
Hugo Herbelin
2014-09-12
*
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-12
*
Fix categorization of recursive inductives.
Matthieu Sozeau
2014-09-10
*
Parsing of Type@{max(i,j)}.
Matthieu Sozeau
2014-09-08
*
Fixing bug #3492.
Pierre-Marie Pédrot
2014-09-07
*
Types declared as Variants really do not accept recursive definitions.
Arnaud Spiwack
2014-09-04
*
Simplify even further the declaration of primitive projections,
Matthieu Sozeau
2014-08-30
*
Fixing commit 50237af2.
Pierre-Marie Pédrot
2014-08-29
*
Fixing bug #3528.
Pierre-Marie Pédrot
2014-08-28
*
Change the way primitive projections are declared to the kernel.
Matthieu Sozeau
2014-08-28
*
- Do module substitution inside mind_record.
Matthieu Sozeau
2014-07-25
*
Properly add a Set lower bound on any polymorphic inductive in Type with
Matthieu Sozeau
2014-07-11
*
Cleanup code related to the constraint solving, which sits now outside the
Matthieu Sozeau
2014-07-03
*
Properly compute the transitive closure of the system of constraints
Matthieu Sozeau
2014-07-03
*
Add toplevel commands to declare global universes and constraints.
Matthieu Sozeau
2014-07-01
*
Fix computation of Type argument for Program's fix_proto.
Matthieu Sozeau
2014-06-24
*
Proofs now take and return an evar_universe_context, simplifying interfaces
Matthieu Sozeau
2014-06-18
*
Removing dead code.
Pierre-Marie Pédrot
2014-06-17
*
- Add "Show Universes" to print information about universes during a proof.
Matthieu Sozeau
2014-06-16
*
Moving hook code from Future to Lemmas. This seemed to disrupt compilation of
Pierre-Marie Pédrot
2014-06-08
[next]