diff options
| author | Vincent Laporte | 2018-10-05 12:56:28 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-10-09 11:17:31 +0000 |
| commit | dae36dcaaaf78e9b09eb644441869008144b451d (patch) | |
| tree | b718deefc8526801e75320151735401e607f2a2f | |
| parent | 94947127d17b33de3109db3b1f3d7944493bd6c3 (diff) | |
[coqchk] Fix case_info for primitive records
| -rw-r--r-- | checker/inductive.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml index 89a5a5196a..5e34f04f51 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -282,6 +282,11 @@ let get_instantiated_arity (ind,u) (mib,mip) params = let elim_sorts (_,mip) = mip.mind_kelim +let is_primitive_record (mib,_) = + match mib.mind_record with + | PrimRecord _ -> true + | NotRecord | FakeRecord -> false + let extended_rel_list n hyps = let rec reln l p = function | LocalAssum _ :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps @@ -381,12 +386,13 @@ let type_case_branches env (pind,largs) (p,pj) c = (* Checking the case annotation is relevant *) let check_case_info env indsp ci = - let (mib,mip) = lookup_mind_specif env indsp in + let mib, mip as spec = lookup_mind_specif env indsp in if not (eq_ind_chk indsp ci.ci_ind) || (mib.mind_nparams <> ci.ci_npar) || (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls) || - (mip.mind_consnrealargs <> ci.ci_cstr_nargs) + (mip.mind_consnrealargs <> ci.ci_cstr_nargs) || + is_primitive_record spec then raise (TypeError(env,WrongCaseInfo(indsp,ci))) (************************************************************************) |