| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
Remaining cases are due to map_constr_with_binders_left_to_right which
does not allow side effects on the evd yet.
|
|
Now the main functions are unify (solves the problems entirely) and
unify_delay and unify_leq (which might leave some unsolved constraints).
Deprecated the_conv_x and the_conv_x_leq (which were misnommers as they
do unification not conversion).
|
|
|
|
|
|
The code is cleaner and more self-explanatory this way.
|
|
It does checking of evar instance and Evd.define, assuming an
occur-check has already been performed.
|
|
|
|
|
|
|
|
|
|
|
|
For second_order_matching call, prefer abstraction of evar arguments,
and use same test as original (just eq_constr)
|
|
Also extend evarconv to handle frozen evars and flags for delta and
betaiota reduction.
- Make evar_conv unification take a record of flags
- Adds an imitate_defs option to evarsolve, deactivated in first-order unification
- Add a way to call back conv_algo differently on types
- We distinguish comparison of terms and types which might be different
w.r.t. delta reductions allowed (everything for types, controlled for
terms). We keep the with_cs flag even for types, to avoid
incompatibilities (in HoTT's theories/Spaces/No.v, the refine in
No_encode_le_lt would diverge due to trying a default canonical
structure during type verification).
- In evarsolve, do_project_effects checks evar instances now
- Solve evar-evar unification using miller patterns if possible.
- FO heuristic in evarconv
- Do not catch critical exceptions in evarconv
- Force HO matching to abstract toplevel evar args,
This disallows K on them, more compatible with w_unify_to_subterm.
- occur_rigidly improvement, better approx of occur-check.
- K_at_toplevel, subterm_ts, betaiota and frozen_evars flags taken into
account in apply_on_subterm and evar_conv_x.
This allow implementing a unification without reduction, e.g. for the
fast path of rewrite subterm selection.
- second_order_matching works up-to cumulativity
- pretyping/coercion: now take unification flags as argument
- pretyping/unification: default_occurrence_test takes a frozen_evars set
export elim_flags_evars to compute frozen evars before elim
- evarsolve: fix evar_define doing check in the wrong order,
as conv_algo can trigger the definition of the evar itself,
define it first in the evd.
- w_unify: disallow HO in consider_remaining. Only used in rewrite now
- use evar_abstraction info
- catch second_order_matching NoOccurrence exception in second_order_matching_with_args
- unify_with_heuristics in API
- second_order_matching: thin evars after abstraction to put in the
right env or fail.
|
|
|
|
This fixes #9484 .
|
|
The semantics is obviously that it is an error if not at least one
occurrence is found (natural semantics for rewriting for
example).
|
|
Named evar_abstract_arguments, this field indicates if the evar
arguments corresponding to certain hypothesis can be immitated during
inversion or not. If the argument comes from an abstraction (the evar
was of arrow type), then imitation is disallowed as it gives unnatural
solutions, and lambda abstraction is preferred.
|
|
Ack-by: SkySkimmer
Reviewed-by: aspiwack
Reviewed-by: ejgallego
Reviewed-by: gares
Reviewed-by: mattam82
Ack-by: maximedenes
|
|
documentation to GH-pages
Reviewed-by: ejgallego
|
|
|
|
In fixpoint typing rule section, a type of constructor is described
twice:
- ∀ p_1:P_1,~… ∀ p_r :P_r,~∀ x_1:T_1,~… ∀ x_r:T_r,~(I_j~p_1 … p_r~t_1 … t_s)
- ∀ p_1:P_1,~…,∀ p_r :P_r,~∀ y_1:B_1,~… ∀ y_k:B_k,~(I~a_1 … a_k)
Both seems invalid.
The former require that the number of parameters and
the number of (non-parameter) constructor argumets is same.
The latter require that the number of (non-parameter) constructor
argumets and the number of inductive type arguments (including paramters) is
same.
Also, "k" is already used for the number of inductive types in
a inductive definition.
So, I changed the number of (non-parameter) constructor
argumets to "m". I choose "m" because "m" is used for the purpose
in the description for iota-reduction of destructors.
Also, I changed the inductive type parameters and arguments of latter
consistent with the former.
|
|
In the description of destructors,
"Type of branches" section and "Typing rule" section shares
the definition of "r" (and "s" from previous commit).
However actual parameters are p_1...p_r in the former section and
q_1...q_r in the latter section.
I guess it's because the latter section uses
p_1...p_l in other purpose: index of constructor for a inductive type.
So, I change the parameter p_1...p_r to q_1...q_r in the former section
to consistent with the latter section.
|
|
In the description of destuctors,
"Type of branches" section uses "p" as the number of arguments.
It is confusing because "p" is used as the number of parameters.
After the section, "Typing rule." section uses "s" without definition as
I q1...qr t1...ts.
It seems that it is the number of arguments.
So, I changed "p" to "s".
"s" is also confusing with sorts, though.
|
|
In Cic admissible rules section, c and c' are exchanged at
https://github.com/coq/coq/commit/8654b03544f0efe4b418a0afdc871ff84784ff83 .
But the exchange is not complete.
This commit complete it.
|
|
|
|
|
|
"'" in the extended (k_i added) form of Fix syntax should be removed.
In the following sentence, A_i' is referenced as A_i.
```
Each :math:`A_i` should be a type (reducible to a term) starting
with at least :math:`k_i` products
:math:`∀ y_1 :B_1 ,~… ∀ y_{k_i} :B_{k_i} ,~A_i'`
```
Also, A_i' is used in ∀ y_1 :B_1 ,~… ∀ y_{k_i} :B_{k_i} ,~A_i' and
A_i' must not equal to ∀ y_1 :B_1 ,~… ∀ y_{k_i} :B_{k_i} ,~A_i'.
The old reference manual, coq-8.7.2-reference-manual.pdf,
doesn't have "'".
They are added by
https://github.com/coq/coq/commit/47dca6c5da585212f69b6b83b25896ff990781e3
which ports Cic document from TeX to sphinx.
So, the change seems just an accident.
|
|
GH-pages
|
|
Related: coq/bignums#17
[ci skip]
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: gares
|
|
Fix #9482
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: vbgl
|
|
print_pure_econstr was not exported (while print_pure_constr was).
|
|
Close #5982 #7388 #7483 #9497
|
|
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: ejgallego
|
|
I forgot to change the profile call; we should find some better
solution but that's OK for now.
|
|
|
|
Fixes #9494.
Was failing with "Cannot create self-referring hypothesis" when
the generated name equaled the eqn.
|
|
Reviewed-by: cpitclaudel
|
|
Reviewed-by: Zimmi48
|
