index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
indschemes.ml
Commit message (
Expand
)
Author
Age
*
[stm] Break stm/toplevel dependency loop.
Emilio Jesus Gallego Arias
2017-02-15
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-02-01
|
\
|
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2017-01-23
|
|
\
|
|
*
Excluding explicitly coinductive types in Scheme Equality (#5284).
Hugo Herbelin
2016-12-23
|
|
*
Fixing anomaly EqUnknown in Equality Scheme (#5278).
Hugo Herbelin
2016-12-22
*
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-02
|
\
|
|
|
*
|
Fix bug #5069: Scheme Equality gives anomalies in sections.
Pierre-Marie Pédrot
2016-10-02
*
|
|
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
|
/
/
*
|
Renaming to more generic has_dependent_elim test
Matthieu Sozeau
2016-07-06
*
|
Move is_prim... to Inductiveops and correct Scheme
Matthieu Sozeau
2016-07-06
*
|
primproj: warning and avoid error.
Matthieu Sozeau
2016-07-06
*
|
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
|
A new infrastructure for warnings.
Maxime Dénès
2016-06-29
*
|
Reuse the typing_flags datatype for inductives.
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
|
\
\
*
|
|
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-09
|
\
\
\
|
|
|
/
|
|
/
|
|
*
|
Adding backtraces to scheme error messages.
Pierre-Marie Pédrot
2016-03-07
*
|
|
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
|
/
/
*
|
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
Univs: generation of induction schemes should not generated useless
Matthieu Sozeau
2015-11-20
*
|
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 environment handling in scheme building.
Matthieu Sozeau
2015-10-02
*
|
Hopefully better names to constructors of internal_flag, as discussed
Hugo Herbelin
2015-09-23
*
|
Improving over 26aa224293 in reporting unexpected error during scheme creation.
Hugo Herbelin
2015-07-27
*
|
Fixing bug #3736 (anomaly instead of error/warning/silence on
Hugo Herbelin
2015-07-27
|
*
Add corresponding field in `VernacInductive`.
Arnaud Spiwack
2015-06-24
|
/
*
Equality Schemes options: reverting commit ff9f94634 which is
Hugo Herbelin
2015-01-24
*
Update headers.
Maxime Dénès
2015-01-12
*
better error message
Enrico Tassi
2014-09-16
*
Type definitions with [Variant] don't generate inductive schemes by default.
Arnaud Spiwack
2014-09-04
*
Print [Variant] types with the keyword [Variant].
Arnaud Spiwack
2014-09-04
*
Simplify even further the declaration of primitive projections,
Matthieu Sozeau
2014-08-30
*
Change the way primitive projections are declared to the kernel.
Matthieu Sozeau
2014-08-28
*
Making code and doc agree on "Set Equality Schemes" (see also bug #2550).
Hugo Herbelin
2014-07-01
*
Safer entry point of primitive projections in the kernel, now it does recognize
Matthieu Sozeau
2014-06-17
*
- Fix RecTutorial, and mutual induction schemes getting the wrong names.
Matthieu Sozeau
2014-05-06
*
- Fix bug preventing apply from unfolding Fixpoints.
Matthieu Sozeau
2014-05-06
*
Adapt universe polymorphic branch to new handling of futures for delayed proofs.
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
*
Qed: feedback when type checking is done
Enrico Tassi
2013-12-24
*
More monomorphic List.mem + List.assoc + ...
letouzey
2013-10-24
*
cList: a few alternative to hashtbl-based uniquize, distinct, subset
letouzey
2013-10-23
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Uniformizing the [if_warn] flag used for warning printing and put
ppedrot
2013-05-08
*
Minor code cleaning in CArray / CList.
ppedrot
2013-03-23
*
Restrict (try...with...) to avoid catching critical exn (part 13)
letouzey
2013-03-13
*
invalid_arg instead of raise (Invalid_argement ...)
letouzey
2013-03-12
[next]