index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
vernac
/
command.ml
Commit message (
Expand
)
Author
Age
*
Fix (partial) #4878: option to stop autodeclaring axiom as instance.
Gaëtan Gilbert
2017-11-28
*
Fix #5347: unify declaration of axioms with and without bound univs.
Gaëtan Gilbert
2017-11-25
*
Use Entries.constant_universes_entry more.
Gaëtan Gilbert
2017-11-24
*
When declaring constants/inductives use ContextSet if monomorphic.
Gaëtan Gilbert
2017-11-24
*
Stop exposing UState.universe_context and its Evd wrapper.
Gaëtan Gilbert
2017-11-24
*
Separate checking univ_decls and obtaining universe binder names.
Gaëtan Gilbert
2017-11-24
*
Use Maps and ids for universe binders
Gaëtan Gilbert
2017-11-24
*
[api] Deprecate Term destructors, move to Constr
Emilio Jesus Gallego Arias
2017-11-22
*
Merge PR #6185: [parser] Remove unnecessary statically initialized hook.
Maxime Dénès
2017-11-21
|
\
*
\
Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 (clause...
Maxime Dénès
2017-11-20
|
\
\
|
|
*
[parser] Remove unnecessary statically initialized hook.
Emilio Jesus Gallego Arias
2017-11-19
|
|
/
|
/
|
*
|
[api] Another large deprecation, `Nameops`
Emilio Jesus Gallego Arias
2017-11-13
|
*
Fixing a remaining "coqdoc" problem with bug #5762 and pr #1120.
Hugo Herbelin
2017-11-08
*
|
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
|
/
*
Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...
Maxime Dénès
2017-10-20
|
\
*
|
[stm] Remove state-handling from Futures.
Emilio Jesus Gallego Arias
2017-10-17
*
|
Fixing #5765 (an anomaly with 'pat in parameters of inductive definition).
Hugo Herbelin
2017-10-05
|
*
Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).
Hugo Herbelin
2017-10-05
|
/
*
Merge PR #688: Binding universe constraints in Definition/Inductive/etc...
Maxime Dénès
2017-09-26
|
\
*
|
[flags] Flag `open Flags`
Emilio Jesus Gallego Arias
2017-09-20
|
*
Don't lose names in UState.universe_context.
Gaëtan Gilbert
2017-09-19
|
*
Allow declaring universe constraints at definition level.
Matthieu Sozeau
2017-09-19
|
/
*
Making detyping potentially lazy.
Pierre-Marie Pédrot
2017-09-04
*
Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name
Maxime Dénès
2017-08-31
|
\
|
*
Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_map
Hugo Herbelin
2017-08-29
*
|
Remove understand_tcc_evars.
Maxime Dénès
2017-08-01
|
/
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-07-04
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
[vernac] Remove forward hooks from Obligations.
Emilio Jesus Gallego Arias
2017-06-20
*
[vernac] Remove unused hooks.
Emilio Jesus Gallego Arias
2017-06-20
*
Clean up universes of constants and inductives
Amin Timany
2017-06-16
*
Fix bugs and add an option for cumulativity
Amin Timany
2017-06-16
*
Fix bugs
Amin Timany
2017-06-16
*
Squashed commit of the following:
Amin Timany
2017-06-16
*
Change the place of inference after sect discharge
Amin Timany
2017-06-16
*
Subtyping inference for inductoves and records
Amin Timany
2017-06-16
*
Add subtyping inference for inductive types
Amin Timany
2017-06-16
*
Using UInfoInd for universes in inductive types
Amin Timany
2017-06-16
*
Extend definition of inductives to include subtyping info
Amin Timany
2017-06-16
*
[proof] Deprecate redundant wrappers.
Emilio Jesus Gallego Arias
2017-06-11
*
Remove the Sigma (monotonous state) API.
Maxime Dénès
2017-06-06
*
Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a sh...
Maxime Dénès
2017-06-06
|
\
*
|
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
*
|
Merge PR#696: Trunk+cleanup constr of global
Maxime Dénès
2017-06-01
|
\
\
*
\
\
Merge PR#561: Improving the Name API
Maxime Dénès
2017-06-01
|
\
\
\
|
*
|
|
Creating a module Nameops.Name extending module Names.Name.
Hugo Herbelin
2017-05-31
|
|
|
*
More precise on preventing clash between bound vars name and hidden impargs.
Hugo Herbelin
2017-05-31
|
|
|
*
Fixing a failure to interpret some local implicit arguments in Inductive.
Hugo Herbelin
2017-05-31
|
|
|
/
|
|
/
|
*
/
|
Support for using type information to infer more precise evar sources.
Hugo Herbelin
2017-05-30
|
/
/
|
*
Command.ml cleanup: remove constr_of_global calls
Matthieu Sozeau
2017-05-29
|
/
[next]