| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
|
|
|
| |
for helping fixing this).
Now the issue is handled solely through refreshing of the terms assigned
to evars during unification.
If ?X = list ?Y, then Y's type is refreshed so that it doesn't mention
a template universe and in turn, ?X won't. Same goes when typechecking
(nil ?X, nil ?Y), the pair constructor levels will be set higher than fresh
universes for the lists carriers. This also handles user-defined functions
on template polymorphic inductives, which was fragile before.
Pretyping and Evd are now uncluttered from template-specific code.
|
| |
|
| |
|
|
|
|
|
|
| |
in Ssreflect).
- Fix is_applied_rewrite_relation to look for propositional relations.
|
| |
|
|
|
|
|
|
|
|
| |
The fix is only partial, because dropping files only works over the menu
bar, the icon bar, the status bar, and so on. Editable boxes, such as the
script widget, catch dnd events, hence preventing this code from working
for these drop targets. Some (labl)gtk expert should be able to sort it
out.
|
|
|
|
|
|
| |
and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml.
The context produced by typechecking a statement is passed in the proof, allowing the
universe name context to be correctly folded as well. Mainly an API cleanup.
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
levels to A and B.
|
|
|
|
|
|
| |
would change the
theory non-trivially.
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
layer. To this intent, we add a cache evar_map in goals that is the
latest known one where the goal is nf-evarized. If the current one
and the cache coincide, we leave the goal as-is.
|
|
|
|
|
| |
Thanks to David M. Cooke on coq-bugs for pointing out one part
of the problem.
|
| |
|
| |
|
| |
|
|
|
|
| |
applications earlier.
|
|
|
|
|
| |
- Fix HoTT coq bug #80, implicit arguments with primitive projections were
wrongly automatically infered.
|
| |
|
|
|
|
|
|
|
| |
a projection constant only of the form
λ params (r : I params), match r with BuildR args => args_i end, without any
other user input and relies on it being typable (no more primitive projections
escaping this).
|
| |
|
| |
|
|
|
|
| |
Fixes bug #3333.
|
|
|
|
|
|
|
| |
it was failing with Not_found before previous commit). This "fixes"
the loop by expanding local defs in "imitate" rather than keeping them
explicit. The example is otherwise too large for me to be able to
understand where does the loop come from.
|
|
|
|
|
| |
fix the type of the term which has to be in the signature of the evar
to declare); some problems remain though (see next commit).
|
|
|
|
| |
- Remove dead code in evarconv.
|
| |
|
| |
|
|
|
|
|
|
| |
Ocaml does not remove the .cmi file if compilation fails, thus causing
subsequent native compilations to fail due to mismatching interfaces.
For the sake of homogeneity, also remove the .cmo/.cmxs file along the way.
|
| |
|
|
|
|
|
| |
bindings of the same variable (fixing HoTT bug #52). Document the unification
of universes in Ltac/tactics.
|
|
|
|
| |
while Context gives different type to each variable, this test-suite file shows this.
|
| |
|
|
|
|
| |
- Move HoTT bug #30 to closed
|
|
|
|
|
|
|
|
| |
of an anomaly in case
a universe inconsistency occurs when applying a coercion. The statement of the test-suite file
cannot check as is, but does check when the correct FunctorCategory is given, instantiating the TypeCat
to Set.
|
|
|
|
|
|
| |
using explicit
universes. The behavior of Hint Rewrite still differs from Hint Resolve though.
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
| |
These options no longer have any impact on the way proofs are loaded. In
other words, loading is always lazy, whatever the options. Keeping them
just so that coqc dies when the user prints some opaque symbol does not
seem worth it.
|
| |
|