diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-17 16:07:37 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-23 01:38:33 +0200 |
commit | 6007579ade085a60664e6b0d4596ff98c51aabf9 (patch) | |
tree | 58c0b5ae6c6f77b31df07e0bd906f56c23ec044a /pretyping/unification.ml | |
parent | c3318ad8408b1ceb0bfd4c2bfedec63ce9324698 (diff) |
Using more general information for primitive records.
This brings more compatibility with handling of mutual primitive records
in the kernel.
Diffstat (limited to 'pretyping/unification.ml')
-rw-r--r-- | pretyping/unification.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 5cf6e4b26..4ba5d2794 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -656,10 +656,12 @@ let rec is_neutral env sigma ts t = let is_eta_constructor_app env sigma ts f l1 term = match EConstr.kind sigma f with - | Construct (((_, i as ind), j), u) when i == 0 && j == 1 -> + | Construct (((_, i as ind), j), u) when j == 1 -> + let open Declarations in let mib = lookup_mind (fst ind) env in (match mib.Declarations.mind_record with - | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Declarations.BiFinite && + | PrimRecord info when mib.Declarations.mind_finite == Declarations.BiFinite && + let (_, projs, _) = info.(i) in Array.length projs == Array.length l1 - mib.Declarations.mind_nparams -> (** Check that the other term is neutral *) is_neutral env sigma ts term @@ -667,11 +669,13 @@ let is_eta_constructor_app env sigma ts f l1 term = | _ -> false let eta_constructor_app env sigma f l1 term = + let open Declarations in match EConstr.kind sigma f with | Construct (((_, i as ind), j), u) -> let mib = lookup_mind (fst ind) env in (match mib.Declarations.mind_record with - | Some (Some (_, projs, _)) -> + | PrimRecord info -> + let (_, projs, _) = info.(i) in let npars = mib.Declarations.mind_nparams in let pars, l1' = Array.chop npars l1 in let arg = Array.append pars [|term|] in |