diff options
author | 2009-05-19 19:10:25 +0000 | |
---|---|---|
committer | 2009-05-19 19:10:25 +0000 | |
commit | 18d4283e4129f6f347970c76d209817f1f66f232 (patch) | |
tree | 9d86a5c16f34d5f5ad384e13b01b03174f5b4e63 /pretyping/unification.ml | |
parent | ebb6a1467c69d8e0a0675852d342ef51cb461a0b (diff) |
Fix in canonical structure resolution: [check_conv_record] may return
non-matching lists.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12133 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/unification.ml')
-rw-r--r-- | pretyping/unification.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 269fb77df..64d96adc9 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -338,15 +338,15 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag (evd', mkMeta mv :: ks, m - 1)) (sigma,[],List.length bs - 1) bs in - let substn = - List.fold_left2 (fun s u1 u -> unirec_rec curenvnb pb b s u1 (substl ks u)) (evd,ms,es) us2 us + let unilist2 f substn l l' = + try List.fold_left2 f substn l l' + with Invalid_argument "List.fold_left2" -> error_cannot_unify (fst curenvnb) sigma (cM,cN) in - let substn = - List.fold_left2 (fun s u1 u -> unirec_rec curenvnb pb b s u1 (substl ks u)) substn params1 params - in - let substn = - List.fold_left2 (unirec_rec curenvnb pb b) substn ts ts1 - in + let substn = unilist2 (fun s u1 u -> unirec_rec curenvnb pb b s u1 (substl ks u)) + (evd,ms,es) us2 us in + let substn = unilist2 (fun s u1 u -> unirec_rec curenvnb pb b s u1 (substl ks u)) + substn params1 params in + let substn = unilist2 (unirec_rec curenvnb pb b) substn ts ts1 in unirec_rec curenvnb pb b substn c1 (applist (c,(List.rev ks))) in |