diff options
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 *) |