index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
inductive.ml
Commit message (
Expand
)
Author
Age
*
Inductive.extract_stack,filter_stack_domain: remove unused arguments
Gaëtan Gilbert
2018-07-03
*
Remove Sorts.contents
Gaëtan Gilbert
2018-06-26
*
Using more general information for primitive records.
Pierre-Marie Pédrot
2018-06-23
*
Reduce circular dependency constants <-> projections
Gaëtan Gilbert
2018-05-31
*
Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec values
Maxime Dénès
2018-03-09
|
\
|
*
Fix SR breakage due to allowing fixpoints on non-rec values
Matthieu Sozeau
2018-03-08
*
|
Update headers following #6543.
Théo Zimmermann
2018-02-27
|
/
*
Fix #6621: Anomaly on fixpoint with primitive projections
Maxime Dénès
2018-01-24
*
[api] Also deprecate constructors of Decl_kinds.
Emilio Jesus Gallego Arias
2017-12-23
*
[lib] Rename Profile to CProfile
Emilio Jesus Gallego Arias
2017-12-09
*
Merge PR #486: Make some functions on terms more robust w.r.t new term constr...
Maxime Dénès
2017-11-24
|
\
|
*
Make some functions on terms more robust w.r.t new term constructs.
Maxime Dénès
2017-11-23
*
|
[api] Deprecate Term destructors, move to Constr
Emilio Jesus Gallego Arias
2017-11-22
|
/
*
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
*
kernel: bugfix in filter_stack_domain.
Matthieu Sozeau
2017-07-26
*
Less footguns in universe handling: remove subst_instance_context.
Pierre-Marie Pédrot
2017-07-11
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Clean up universes of constants and inductives
Amin Timany
2017-06-16
*
Using UInfoInd for universes in inductive types
Amin Timany
2017-06-16
*
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
*
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-27
*
Introducing contexts parameterized by the inner term type.
Pierre-Marie Pédrot
2017-02-14
*
Merge remote-tracking branch 'gforge/v8.5' into v8.6
Matthieu Sozeau
2016-07-26
|
\
|
*
Fix bug #4876: critical bug in guard condition checker.
Matthieu Sozeau
2016-07-25
*
|
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
|
Separate flags for fix/cofix/match reduction and clean reduction function names.
Maxime Dénès
2016-07-01
*
|
Moving the typing_flags to the environment.
Pierre-Marie Pédrot
2016-06-18
*
|
Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.
Pierre-Marie Pédrot
2016-06-16
|
\
\
|
*
|
Assume totality: dedicated type rather than bool
Arnaud Spiwack
2016-06-14
*
|
|
Removing OCaml deprecated function names from the Lazy module.
Pierre-Marie Pédrot
2016-03-10
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-05
|
\
\
\
|
|
|
/
|
|
/
|
|
*
|
This fix is probably not enough to justify that there are no problems with
Maxime Dénès
2016-03-04
*
|
|
CLEANUP: Simplifying the changes done in "kernel/*"
Matej Kosik
2016-02-15
*
|
|
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
|
*
|
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
|
merge
Matej Kosik
2016-01-11
|
\
\
\
|
*
|
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
*
|
|
|
Removing dead code.
Pierre-Marie Pédrot
2015-12-27
|
/
/
/
*
|
|
Unifying betazeta_applist and prod_applist into a clearer interface.
Hugo Herbelin
2015-12-05
*
|
|
Moving extended_rel_vect/extended_rel_list to the kernel.
Hugo Herbelin
2015-12-05
*
|
|
Contracting one extra beta-redex on the fly when typing branches of "match".
Hugo Herbelin
2015-12-05
*
|
|
A few renaming and simplification in inductive.ml.
Hugo Herbelin
2015-12-05
|
/
/
*
|
Univs: be more restrictive for template polymorphic constants: only
Matthieu Sozeau
2015-10-12
*
|
Univs: fix bug #4251, handling of template polymorphic constants.
Matthieu Sozeau
2015-10-02
*
|
Univs/Inductive: fix typechecking of cases
Matthieu Sozeau
2015-07-15
*
|
Unused variables reported by OCaml.
Hugo Herbelin
2015-07-10
*
|
Kernel/Checker: Cleanup fixes of substitutions due to let-ins.
Matthieu Sozeau
2015-07-09
*
|
Template polymorphism: A bug-fix for Bug #4258
mlasson
2015-07-09
*
|
Univs: bug fix.
Matthieu Sozeau
2015-07-07
[next]