diff options
| author | Matthieu Sozeau | 2014-08-14 13:01:30 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-08-14 13:01:30 +0200 |
| commit | 37a58edffeff7b6a7f03ec781e1e2ca73de4b3af (patch) | |
| tree | e7c73845d8ccc700662875c5455d9a797225da87 /pretyping | |
| parent | 9c1e76422c63ab845d72893ca85dd38ce5ce9bec (diff) | |
Restrict eta-conversion to inductive records, fixing bug #3310.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index ed04c71503..68dfb1a1bd 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -745,21 +745,21 @@ and conv_record trs env evd (ctx,(h,h'),c,bs,(params,params1),(us,us2),(ts,ts1), and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with - | Some (exp,projs) when Array.length projs > 0 -> + | Some (exp,projs) when Array.length projs > 0 + && mib.Declarations.mind_finite -> let pars = mib.Declarations.mind_nparams in (try let l1' = Stack.tail pars sk1 in - if Environ.is_projection projs.(0) env then - let l2' = - let term = Stack.zip (term2,sk2) in - List.map (fun p -> mkProj (p, term)) (Array.to_list projs) - in - exact_ise_stack2 env evd (evar_conv_x ts) l1' - (Stack.append_app_list l2' Stack.empty) - else raise (Failure "") + let l2' = + let term = Stack.zip (term2,sk2) in + List.map (fun p -> mkProj (p, term)) (Array.to_list projs) + in + exact_ise_stack2 env evd (evar_conv_x ts) l1' + (Stack.append_app_list l2' Stack.empty) with - | Invalid_argument _ (* Stack.tail: partially applied constructor *) - | Failure _ -> UnifFailure(evd,NotSameHead)) + | Invalid_argument _ -> + (* Stack.tail: partially applied constructor *) + UnifFailure(evd,NotSameHead)) | _ -> UnifFailure (evd,NotSameHead) (* Profiling *) |