diff options
| author | Matthieu Sozeau | 2016-03-16 18:00:25 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-03-16 18:05:42 +0100 |
| commit | bfce815bd1fa2c603141661b209a864c67ae1dbf (patch) | |
| tree | 64d2897047a845274845b4b3ffc585602841514c | |
| parent | 34c467a4e41e20a9bf1318d47fbc09da94c5ad97 (diff) | |
Fix incorrect behavior of CS resolution
Due to a change in pretyping, using cast annotations as typing
constraints, the canonical structure problems given to the unification
could contain non-evar-normalized terms, hence we force
evar normalization where necessary to ensure the same CS solutions
can be found. Here the dependency test is fooled by an erasable
dependency, and the following resolution needs a independent codomain
for pop b to be well-scoped.
| -rw-r--r-- | pretyping/evarconv.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 690b974be5..b8d92b9be7 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -138,6 +138,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = try match kind_of_term t2 with Prod (_,a,b) -> (* assert (l2=[]); *) + let _, a, b = destProd (Evarutil.nf_evar sigma t2) in if dependent (mkRel 1) b then raise Not_found else lookup_canonical_conversion (proji, Prod_cs), (Stack.append_app [|a;pop b|] Stack.empty) |