diff options
| author | Gaëtan Gilbert | 2018-06-11 13:57:28 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 15:46:16 +0100 |
| commit | 06b29ed748a9d9b99c2c08a3788906dbad5417d2 (patch) | |
| tree | 5623fad28f68f9450ab7122f595ec1727f8f52bf /pretyping | |
| parent | 71b9ad8526155020c8451dd326a52e391a9a8585 (diff) | |
Repair relevance marks in-kernel.
Prevent errors when under annotating binders.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/inductiveops.ml | 2 | ||||
| -rw-r--r-- | pretyping/inferCumulativity.ml | 2 | ||||
| -rw-r--r-- | pretyping/typing.ml | 6 |
3 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 204618034e..678aebfbe6 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -468,7 +468,7 @@ let compute_projections env (kn, i as ind) = anomaly Pp.(str "Trying to build primitive projections for a non-primitive record") | PrimRecord info -> let id, _, _, _ = info.(i) in - make_annot (Name id) mib.mind_packets.(i).mind_relevant + make_annot (Name id) mib.mind_packets.(i).mind_relevance in let pkt = mib.mind_packets.(i) in let { mind_nparams = nparamargs; mind_params_ctxt = params } = mib in diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml index bf8a38a353..fefc15dfb2 100644 --- a/pretyping/inferCumulativity.ml +++ b/pretyping/inferCumulativity.ml @@ -201,7 +201,7 @@ let infer_inductive env mie = Array.fold_left (fun variances u -> LMap.add u Variance.Irrelevant variances) LMap.empty uarray in - let env = Typeops.check_context env params in + let env, params = Typeops.check_context env params in let variances = List.fold_left (fun variances entry -> let variances = infer_arity_constructor true env variances entry.mind_entry_arity diff --git a/pretyping/typing.ml b/pretyping/typing.ml index b660973cdd..89f72c874b 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -397,7 +397,7 @@ let rec execute env sigma cstr = | Lambda (name,c1,c2) -> let sigma, j = execute env sigma c1 in let sigma, var = type_judgment env sigma j in - let () = check_binder_annot env var.utj_type name in + let name = check_binder_annot var.utj_type name in let env1 = push_rel (LocalAssum (name, var.utj_val)) env in let sigma, j' = execute env1 sigma c2 in sigma, judge_of_abstraction env1 name.binder_name var j' @@ -405,7 +405,7 @@ let rec execute env sigma cstr = | Prod (name,c1,c2) -> let sigma, j = execute env sigma c1 in let sigma, varj = type_judgment env sigma j in - let () = check_binder_annot env varj.utj_type name in + let name = check_binder_annot varj.utj_type name in let env1 = push_rel (LocalAssum (name, varj.utj_val)) env in let sigma, j' = execute env1 sigma c2 in let sigma, varj' = type_judgment env1 sigma j' in @@ -416,7 +416,7 @@ let rec execute env sigma cstr = let sigma, j2 = execute env sigma c2 in let sigma, j2 = type_judgment env sigma j2 in let sigma, _ = judge_of_cast env sigma j1 DEFAULTcast j2 in - let () = check_binder_annot env j2.utj_type name in + let name = check_binder_annot j2.utj_type name in let env1 = push_rel (LocalDef (name, j1.uj_val, j2.utj_val)) env in let sigma, j3 = execute env1 sigma c3 in sigma, judge_of_letin env name.binder_name j1 j2 j3 |