index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
pretyping
/
retyping.ml
Age
Commit message (
Expand
)
Author
2020-11-16
Extend hack to use postponed constraints in retyping to template poly
Gaëtan Gilbert
2020-07-08
Merge PR #12627: Fix Canonical with universe polymorphism and primitive proje...
Enrico Tassi
2020-07-06
Primitive persistent arrays
Maxime Dénès
2020-07-05
Fix Canonical with universe polymorphism and primitive projection
Gaëtan Gilbert
2020-07-01
UIP in SProp
Gaëtan Gilbert
2020-05-10
No more local reduction functions in Reductionops.
Pierre-Marie Pédrot
2020-03-28
Remove some cruft from Reductionops API.
Pierre-Marie Pédrot
2020-03-18
Rename Retypeops -> Relevanceops
Gaëtan Gilbert
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2020-02-14
Use thunks to univ instead of lazy constr for template typing
Gaëtan Gilbert
2019-11-22
Use the relevance flag in CClosure rel contexts in an efficient way.
Pierre-Marie Pédrot
2019-11-21
[coq] Untabify the whole ML codebase.
Emilio Jesus Gallego Arias
2019-11-01
Add primitive float computation in Coq kernel
Guillaume Bertholon
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-04-10
Remove calls to global env in Inductiveops
Maxime Dénès
2019-03-14
Add relevance marks on binders.
Gaëtan Gilbert
2019-03-14
Add a non-cumulative impredicative universe SProp.
Gaëtan Gilbert
2019-03-14
Make Sorts.t private
Gaëtan Gilbert
2019-02-04
Primitive integers
Maxime Dénès
2018-10-31
Renaming is_template_polymorphic -> is_template_polymorphic_ind.
Hugo Herbelin
2018-06-26
Remove Sorts.contents
Gaëtan Gilbert
2018-04-13
Evar maps contain econstrs.
Gaëtan Gilbert
2018-03-31
[econstr] Forbid calling `to_constr` in open terms.
Emilio Jesus Gallego Arias
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-12-09
[lib] Rename Profile to CProfile
Emilio Jesus Gallego Arias
2017-11-28
Adding a variant get_truncation_family_of of get_sort_family_of.
Hugo Herbelin
2017-11-28
Moving non-recursive function sort_family_of out of the retype block of recur...
Hugo Herbelin
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-09-28
Remove trivial TODO comment (constants can't be template poly now).
Gaëtan Gilbert
2017-07-26
Removing template polymorphism for definitions.
Pierre-Marie Pédrot
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-02
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-04-01
Using delayed universe instances in EConstr.
Pierre-Marie Pédrot
2017-04-01
Actually exporting delayed universes in the EConstr implementation.
Pierre-Marie Pédrot
2017-02-14
Definining EConstr-based contexts.
Pierre-Marie Pédrot
2017-02-14
Removing compatibility layers in Retyping
Pierre-Marie Pédrot
2017-02-14
Reductionops now return EConstrs.
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
Cleaning up opening of the EConstr module in pretyping folder.
Pierre-Marie Pédrot
2017-02-14
Making judgment type generic over the type of inner constrs.
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
2017-02-14
Termops API using EConstr.
Pierre-Marie Pédrot
2016-08-24
CLEANUP: minor readability improvements
Matej Kosik
2016-07-03
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-01
Separate flags for fix/cofix/match reduction and clean reduction function names.
Maxime Dénès
2016-02-09
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-01-20
Update copyright headers.
Maxime Dénès
2015-11-25
Reverting 1467c225 (Fixing an old typo in Retyping, found by Matej).
Hugo Herbelin
[next]
