index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
pretyping
Age
Commit message (
Expand
)
Author
2017-08-29
Merge PR #946: Functional pretyping interface
Maxime Dénès
2017-08-16
Merge PR #841: Timorous fix of bug #5598 on global existing class in sections
Maxime Dénès
2017-08-01
Remove understand_tcc_evars.
Maxime Dénès
2017-08-01
Move type_uconstr to Tacinterp.
Maxime Dénès
2017-08-01
Remove understand_judgment and understand_judgment_tcc.
Maxime Dénès
2017-08-01
Remove allow_anonymous_refs.
Maxime Dénès
2017-08-01
Remove pure_open_constr (now open_constr)
Maxime Dénès
2017-08-01
Move glob_constr_ltac_closure to evar_refiner.
Maxime Dénès
2017-08-01
Merge PR #913: Less allocations in Detyping
Maxime Dénès
2017-08-01
Merge PR #806: closing bug 5315
Maxime Dénès
2017-07-31
Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead
Maxime Dénès
2017-07-29
closing bug 5315
Julien Forest
2017-07-27
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-26
Add a comment regarding the specialization of the combinator in Detyping.
Pierre-Marie Pédrot
2017-07-26
Removing template polymorphism for definitions.
Pierre-Marie Pédrot
2017-07-21
Allocation-friendly detyping of term arrays.
Pierre-Marie Pédrot
2017-07-20
Merge branch 'v8.7'
Maxime Dénès
2017-07-13
Remove the function Global.type_of_global_unsafe.
Pierre-Marie Pédrot
2017-07-13
Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.
Pierre-Marie Pédrot
2017-07-13
Getting rid of AUContext abstraction breakers in Discharge.
Pierre-Marie Pédrot
2017-07-13
Make the typeclass implementation fully compatible with universe polymorphism.
Pierre-Marie Pédrot
2017-07-13
Safer API for Global.type_of_global_in_context.
Pierre-Marie Pédrot
2017-07-13
Getting rid of AUContext abstraction breakers in Recordops.
Pierre-Marie Pédrot
2017-07-13
Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: Kernel
Maxime Dénès
2017-07-11
Deprecate options that were introduced for compatibility with 8.5.
Théo Zimmermann
2017-07-11
Safe API for accessing universe constraints of global references.
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-07
Merge PR #863: Fixing environment in warning "Projection value has no head co...
Maxime Dénès
2017-07-07
Fixing environment in warning "Projection value has no head constant".
Hugo Herbelin
2017-07-04
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-28
A fix for #5598 (no discharge of Existing Classes referring to local variables).
Hugo Herbelin
2017-06-28
Avoiding an optional int rather than using -1 to encode a local flag.
Hugo Herbelin
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 a bug
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-16
Use inductive subtyping for conv/cumul
Amin Timany
2017-06-16
Subtyping inference for inductoves and records
Amin Timany
2017-06-16
Using UInfoInd for universes in inductive types
Amin Timany
2017-06-15
Merge PR#713: Bump year in headers.
Maxime Dénès
2017-06-15
Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraints
Maxime Dénès
2017-06-15
Merge PR#375: Deprecation
Maxime Dénès
2017-06-14
Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").
Maxime Dénès
2017-06-14
Deprecate options that were introduced for compatibility with 8.2.
Guillaume Melquiond
2017-06-14
Remove options deprecated since 8.4.
Guillaume Melquiond
[next]
