index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
pretyping
/
inductiveops.mli
Age
Commit message (
Expand
)
Author
2018-06-27
Swapping Context and Constr: defining declarations on constr in Constr.
Hugo Herbelin
2018-06-17
Remove the proj_body field from the kernel.
Pierre-Marie Pédrot
2018-06-17
Remove the proj_eta field of the kernel.
Pierre-Marie Pédrot
2018-03-28
[api] Deprecate a couple of aliases that we missed.
Emilio Jesus Gallego Arias
2018-03-05
Merge PR #6855: Update headers following #6543.
Maxime Dénès
2018-02-28
[econstr] Continue consolidation of EConstr API under `interp`.
Emilio Jesus Gallego Arias
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-02-11
Use specialized function for inductive subtyping inference.
Gaëtan Gilbert
2018-02-10
Inference of inductive subtyping does not need an evar map.
Gaëtan Gilbert
2017-11-26
[api] Remove aliases of `Evar.t`
Emilio Jesus Gallego Arias
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-16
Fix bugs
Amin Timany
2017-06-16
Subtyping inference for inductoves and records
Amin Timany
2017-04-01
Using delayed universe instances in EConstr.
Pierre-Marie Pédrot
2017-02-14
Namegen primitives now apply on evar constrs.
Pierre-Marie Pédrot
2017-02-14
Eliminating parts of the right-hand side compatibility layer
Pierre-Marie Pédrot
2017-02-14
Leminv API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Tactics API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Cases API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Retyping API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Reductionops API using EConstr.
Pierre-Marie Pédrot
2016-07-06
Disallow dependent case on prim records w/o eta
Matthieu Sozeau
2016-07-06
Renaming to more generic has_dependent_elim test
Matthieu Sozeau
2016-07-06
Move is_prim... to Inductiveops and correct Scheme
Matthieu Sozeau
2016-01-21
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2016-01-11
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2015-12-05
An example in centralizing similar functions to a common place so that
Hugo Herbelin
2015-07-05
Fix handling of primitive projections in VM.
Maxime Dénès
2015-03-25
Fully fixing bug #3491 (anomaly when building _rect scheme in the
Hugo Herbelin
2015-01-12
Update headers.
Maxime Dénès
2014-08-28
Change the way primitive projections are declared to the kernel.
Matthieu Sozeau
2014-08-14
Fix non-printing of coercions for primitive projections (fixes bug #3433).
Matthieu Sozeau
2014-08-05
A new step in the new "standard" naming policy for propositional hypotheses
Hugo Herbelin
2014-08-03
Move to a representation of universe polymorphic constants using indices for ...
Matthieu Sozeau
2014-08-01
Continuing (incomplete) cleaning of Inductiveops.
Hugo Herbelin
2014-08-01
A tentative uniform naming policy in module Inductiveops.
Hugo Herbelin
2014-06-01
Use of "H"-based names for propositional hypotheses obtained by
Hugo Herbelin
2014-05-31
Dead code + typo.
Hugo Herbelin
2014-05-06
Initial work on reintroducing old-style polymorphism for compatibility (the s...
Matthieu Sozeau
2014-05-06
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2013-04-29
Merging Context and Sign.
ppedrot
2013-04-29
Splitting Term into five unrelated interfaces:
ppedrot
2012-08-08
Updating headers.
herbelin
2012-03-02
"Let in" in pattern hell, one more iteration
pboutill
2012-01-16
Inductiveops.nb_*{,_env} cleaning
pboutill
2011-12-18
Granted legitimate wish #2607 (not exposing crude fixpoint body of
herbelin
2011-04-06
A few extra combinators about rel_declaration/named_declaration + a bit of doc
herbelin
[next]
