diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 2 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 10 | ||||
| -rw-r--r-- | pretyping/recordops.mli | 2 | ||||
| -rw-r--r-- | pretyping/unification.ml | 4 |
4 files changed, 11 insertions, 7 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 236bc1b43..47822b22e 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -324,7 +324,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = if the first argument is a beta-redex (expand a constant only if necessary) or the second argument is potentially usable as a canonical projection *) - if isLambda flex1 or is_open_canonical_projection i appr2 + if isLambda flex1 or is_open_canonical_projection env i appr2 then match eval_flexible_term ts env flex1 with | Some v1 -> diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 994fe33d0..b3be7afd9 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -336,10 +336,14 @@ let declare_canonical_structure ref = let lookup_canonical_conversion (proj,pat) = List.assoc pat (Refmap.find proj !object_table) -let is_open_canonical_projection sigma (c,args) = +let is_open_canonical_projection env sigma (c,args) = try - let n = find_projection_nparams (global_of_constr c) in - try isEvar_or_Meta (whd_evar sigma (List.nth args n)) with Failure _ -> false + let n = find_projection_nparams (global_of_constr c) in + try + let arg = whd_betadeltaiota env sigma (List.nth args n) in + let hd = match kind_of_term arg with App (hd, _) -> hd | _ -> arg in + not (isConstruct hd) + with Failure _ -> false with Not_found -> false let freeze () = diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index b4e76756b..6165fac26 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -80,6 +80,6 @@ val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds val lookup_canonical_conversion : (global_reference * cs_pattern) -> obj_typ val declare_canonical_structure : global_reference -> unit val is_open_canonical_projection : - Evd.evar_map -> (constr * constr list) -> bool + Environ.env -> Evd.evar_map -> (constr * constr list) -> bool val canonical_projections : unit -> ((global_reference * cs_pattern) * obj_typ) list diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 6fff81cfe..693ea4395 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -560,7 +560,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag let f1 () = if isApp cM then let f1l1 = decompose_app cM in - if is_open_canonical_projection sigma f1l1 then + if is_open_canonical_projection env sigma f1l1 then let f2l2 = decompose_app cN in solve_canonical_projection curenvnb pb b cM f1l1 cN f2l2 substn else error_cannot_unify (fst curenvnb) sigma (cM,cN) @@ -573,7 +573,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag try f1 () with e when precatchable_exception e -> if isApp cN then let f2l2 = decompose_app cN in - if is_open_canonical_projection sigma f2l2 then + if is_open_canonical_projection env sigma f2l2 then let f1l1 = decompose_app cM in solve_canonical_projection curenvnb pb b cN f2l2 cM f1l1 substn else error_cannot_unify (fst curenvnb) sigma (cM,cN) |