index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
pretyping
/
evarconv.ml
Age
Commit message (
Expand
)
Author
2018-06-23
Merge PR #7827: [engine] safe [add_unification_pb] interface
Pierre-Marie Pédrot
2018-06-23
Using more general information for primitive records.
Pierre-Marie Pédrot
2018-06-15
evd/evarutil: safe [add_unification_pb] interface, taking EConstr's
Matthieu Sozeau
2018-06-04
Stronger invariants in unification signature.
Pierre-Marie Pédrot
2018-05-17
Split off Universes functions dealing with generating new universes.
Gaëtan Gilbert
2018-05-11
set_solve_evars doesn't use an evar_map ref
Gaëtan Gilbert
2018-05-11
Deprecate most evarutil evdref functions
Gaëtan Gilbert
2018-04-13
Evar maps contain econstrs.
Gaëtan Gilbert
2018-03-09
Cumulativity: improve treatment of irrelevant universes.
Gaëtan Gilbert
2018-03-09
Allow using cumulativity without forcing strict constraints.
Gaëtan Gilbert
2018-03-08
Leave cumul constructor universes as is during unif
Matthieu Sozeau
2018-03-08
Relax conversion of constructors according to the pCuIC model
Matthieu Sozeau
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-02-10
Simplification: cumulativity information is variance information.
Gaëtan Gilbert
2018-01-19
Define EConstr version of [push_rec_types].
Cyprien Mangin
2017-12-23
[api] Also deprecate constructors of Decl_kinds.
Emilio Jesus Gallego Arias
2017-12-15
Fix #5368: Canonical structure unification fails.
Pierre-Marie Pédrot
2017-12-09
[lib] Rename Profile to CProfile
Emilio Jesus Gallego Arias
2017-12-06
Getting rid of the Update constructor in Reductionops.
Pierre-Marie Pédrot
2017-12-06
Getting rid of the Shift constructor in Reductionops.
Pierre-Marie Pédrot
2017-11-22
[api] Deprecate Term destructors, move to Constr
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-10-17
Properly handling projection parameters in canonical structures.
Pierre-Marie Pédrot
2017-10-17
Handling primitive projections in canonical structures.
Pierre-Marie Pédrot
2017-07-13
Getting rid of AUContext abstraction breakers in Recordops.
Pierre-Marie Pédrot
2017-07-11
Less footguns in universe handling: remove subst_instance_context.
Pierre-Marie Pédrot
2017-07-11
Getting rid of simple calls to AUContext.instance.
Pierre-Marie Pédrot
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-16
Fix a bug in cumulativity
Amin Timany
2017-06-16
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
Make unification use subtyping info of inductives
Amin Timany
2017-06-06
Remove the Sigma (monotonous state) API.
Maxime Dénès
2017-06-02
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
Don't double up on periods in anomalies
Jason Gross
2017-05-31
Creating a module Nameops.Name extending module Names.Name.
Hugo Herbelin
2017-05-29
Merge PR#512: [cleanup] Unify all calls to the error function.
Maxime Dénès
2017-05-27
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-27
[coqlib] Move `Coqlib` to `library/`.
Emilio Jesus Gallego Arias
2017-05-25
Merge PR#481: [option] Remove support for non-synchronous options.
Maxime Dénès
2017-05-24
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-24
[option] Remove support for non-synchronous options.
Emilio Jesus Gallego Arias
2017-04-27
Remove unused [open] statements
Gaetan Gilbert
2017-04-25
[location] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-04-25
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-07
Merge branch 'master' into econstr
Pierre-Marie Pédrot
2017-04-05
Removing a normalization hotspot from EConstr.
Pierre-Marie Pédrot
[next]
