| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
I had to reorganize the code a bit. The Context command moved to
comAssumption, as it is not so related to type classes. We were able to
remove a few hooks on the way.
|
|
|
|
One other call still remains, but will require to refactor some
section-handling code.
|
|
|
|
As per the OCaml documentation, the order for maps should be total.
I also remove some circumvolutions that were added around eliminators
and canonical names because of this incorrect order.
|
|
We already have indirection (constant -> effect name, effect name ->
function) so we only need to stop using summary.ref for the second map.
|
|
Reviewed-by: gares
|
|
This was making an assertion fail on
https://github.com/coq/coq/issues/9684 after 23f84f37
|
|
This cache makes the pretyper depend on components that should morally
be higher-level (Libobject and co), so I'd like to see how critical this
cache is before taking any action.
|
|
Ack-by: jfehrle
Ack-by: ppedrot
Reviewed-by: vbgl
|
|
Ack-by: JasonGross
Reviewed-by: ppedrot
|
|
We provide a flag that allows for a dumber but O(log n) algorithm generating
fresh names in detyping.
|
|
For now it does not change anything, but it will make the move towards a
faster algorithm seamless.
|
|
There was a hidden bug to an unexpected variable capture in decomp_branch.
Let us use proper structures to avoid this kind of mess.
|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
(warn if bar is a nonprimitive projection)
|
|
|
|
|
|
only.
Ack-by: SkySkimmer
Reviewed-by: aspiwack
Ack-by: ejgallego
Ack-by: gares
Ack-by: herbelin
Reviewed-by: mattam82
Ack-by: maximedenes
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: gares
Ack-by: pi8027
|
|
|
|
In particular evar_eqappr_x tries to find a miller pattern on both sides,
while the fast path for evars tries solve_simple_eqn in one direction
only. So if you have (Evar-not-miller = Evar-miller) the code was not
trying to solve the RHS.
|
|
Previously, they were hard-wired in the ML code.
|
|
This option made the Coercions command follow non-standard scoping rules
(effect on `Require` rather than `Import`). It was already marked for deletion
in 8.8.
|
|
|
|
The `Coercion` command did report many ambiguous paths when one declared
multiple inheritances. This change makes the `Coercion` command to do not
report them when
1. all the coercion in the potentially ambiguous paths respect the uniform
inheritance condition and
2. functional compositions of the potentially ambiguous paths are convertible to
each other.
The first condition is not explicitly checked but is used to make the checking
process of the second condition easy.
The key idea of this change:
Let us consider a sequence of coercion
f_1 : C_1 >-> C_2, f_2 : C_2 >-> C_3, ..., f_n : C_n >-> C_(n+1)
which respect the uniform inheritance condition and where the user-defined
classes C_i have m_i parameters respectively (i <= n).
The functional composition f_1 . ... . f_n can be expressed as follows:
(fun x_1 ... x_(m_1) y =>
f_n _ ... _ (* m_n times repetition of holes *)
(...
(f_2 _ ... _ (* m_2 times repetition of holes *)
(f_1 x_1 ... x_(m_1) y))...)),
and the contents of all the holes can be determined (inferred) without leaving
any existential variables in them thanks to the uniform inheritance condition.
Misc:
- A test case for this change: test-suite/output/relaxed_ambiguous_paths.v
- Turn the ambiguous paths messages into warnings to do output test.
|
|
Prevent errors when under annotating binders.
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
|
Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Ack-by: ppedrot
|
|
Ack-by: gares
Ack-by: herbelin
Ack-by: mattam82
Ack-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
It used to simply remember the normal form of the type of the constructor.
This is somewhat problematic as this is ambiguous in presence of
let-bindings. Rather, we store this data in a fully expanded way, relying
on rel_contexts.
Probably fixes a crapload of bugs with inductive types containing
let-bindings, but it seems that not many were reported in the bugtracker.
|
|
See #9616
|
|
|
|
Reviewed-by: ejgallego
Ack-by: herbelin
Reviewed-by: mattam82
|
|
This is because it can raise Not_found in depth and we need to catch
it at the right time.
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
I think the usage looks cleaner this way.
|
|
|
|
|
|
|
