diff options
| author | Maxime Dénès | 2018-10-24 16:30:02 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-11-06 14:19:38 +0100 |
| commit | 732476594f19be0125a553b1c6135d57995c63c2 (patch) | |
| tree | 9fbccd358e45c0cc001248d26738f295e48484b1 | |
| parent | a1bdaf0635b5d5b9e007662f324dd526ba0fe8d3 (diff) | |
[checker] Fix "error related to inductive types"
| -rw-r--r-- | checker/checkInductive.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index cf086049ca..4e026d6f60 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -89,7 +89,8 @@ let typecheck_arity env params inds = env_ar') env inds in - env_arities + let env_ar_par = push_rel_context params env_arities in + env_arities, env_ar_par (* Check that the subtyping information inferred for inductive types in the block is correct. *) (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) @@ -252,7 +253,7 @@ let check_inductive env kn mib = user_err Pp.(str "number the right number of parameters"); (* mind_packets *) (* - check arities *) - let env_ar = typecheck_arity env0 params mib.mind_packets in + let env_ar, env_ar_par = typecheck_arity env0 params mib.mind_packets in (* - check constructor types *) Array.iter (typecheck_one_inductive env_ar params) mib.mind_packets; (* check the inferred subtyping relation *) @@ -263,8 +264,8 @@ let check_inductive env kn mib = check_subtyping acumi params env_ar mib.mind_packets in (* check mind_nparams_rec: positivity condition *) - let packets = Array.map (fun p -> (p.mind_typename, Array.to_list p.mind_consnames, p.mind_user_lc, (p.mind_arity_ctxt,()))) mib.mind_packets in - let _ = Indtypes.check_positivity ~chkpos:true kn env_ar mib.mind_params_ctxt mib.mind_finite packets in + let packets = Array.map (fun p -> (p.mind_typename, Array.to_list p.mind_consnames, p.mind_user_lc, (p.mind_arity_ctxt,p.mind_arity))) mib.mind_packets in + let _ = Indtypes.check_positivity ~chkpos:true kn env_ar_par mib.mind_params_ctxt mib.mind_finite packets in (* check mind_equiv... *) (* Now we can add the inductive *) add_mind kn mib env |