index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
library
/
declare.ml
Commit message (
Expand
)
Author
Age
*
[general] Move files to directories matching linking order.
Emilio Jesus Gallego Arias
2017-07-19
*
Getting rid of AUContext abstraction breakers in Discharge.
Pierre-Marie Pédrot
2017-07-13
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
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
*
Change the place of inference after sect discharge
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
*
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
*
Don't double up on periods in anomalies
Jason Gross
2017-06-02
*
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-24
|
\
|
*
Allow flexible anonymous universes in instances and sorts.
Gaetan Gilbert
2017-05-03
*
|
[location] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-04-25
*
|
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-25
|
/
*
Moving Universes to the engine/ folder.
Pierre-Marie Pédrot
2016-10-30
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-24
|
\
|
*
Merge branch 'bug5036' into v8.6
Matthieu Sozeau
2016-10-20
|
|
\
|
|
*
Fix bug #5036 autorewrite, sections and universes
Matthieu Sozeau
2016-10-20
*
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-02
|
\
|
|
|
*
|
Merge remote-tracking branch 'github/pr/299' into v8.6
Maxime Dénès
2016-09-30
|
|
\
\
|
*
|
|
Fix bug #5036 autorewrite, sections and universes
Matthieu Sozeau
2016-09-29
|
|
|
/
|
|
/
|
|
|
*
Fix bug #4869, allow Prop, Set, and level names in constraints.
Matthieu Sozeau
2016-09-29
|
|
/
*
|
Revert "Merge remote-tracking branch 'github/pr/283' into trunk"
Maxime Dénès
2016-09-22
*
|
Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.
Maxime Dénès
2016-09-20
*
|
Stylistic improvements in intf/decl_kinds.mli.
Maxime Dénès
2016-09-20
*
|
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
*
|
Unify location handling of error functions.
Emilio Jesus Gallego Arias
2016-08-19
|
/
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Reuse the typing_flags datatype for inductives.
Pierre-Marie Pédrot
2016-06-18
*
Moving the typing_flags to the environment.
Pierre-Marie Pédrot
2016-06-18
*
Factorizing the uses of Declareops.safe_flags.
Pierre-Marie Pédrot
2016-06-16
*
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
*
|
Univs: more robust Universe/Constraint decls #4816
Matthieu Sozeau
2016-06-13
*
|
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-29
|
\
\
|
*
|
Fix bug #4503: mixing universe polymorphic and monomorphic
Matthieu Sozeau
2016-01-23
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
|
*
|
Update copyright headers.
Maxime Dénès
2016-01-20
|
*
|
Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.
Maxime Dénès
2016-01-15
*
|
|
Changing "P is assumed" to "P is declared".
Hugo Herbelin
2016-01-14
*
|
|
Remove some useless type declarations.
Guillaume Melquiond
2016-01-02
|
/
/
*
|
Univs: entirely disallow instantiation of polymorphic constants with
Matthieu Sozeau
2015-11-27
*
|
Add a way to get the right fix_exn in external vernacular commands
Matthieu Sozeau
2015-10-30
*
|
Avoid type checking private_constants (side_eff) again during Qed (#4357).
Enrico Tassi
2015-10-28
*
|
Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names
Matthieu Sozeau
2015-10-27
*
|
Univs: Change intf of push_named_def to return the computed universe
Matthieu Sozeau
2015-10-02
*
|
Univs: refined handling of assumptions
Matthieu Sozeau
2015-10-02
*
|
Univs: fix Universe vernacular, fix bug #4287.
Matthieu Sozeau
2015-10-02
[next]