Fix some relevances.

Author: ppedrot

src/parametricity.ml

@@ -335,7 +335,8 @@ let rec relation order evd env (t : constr) : constr =
  debug_mode := false;
  let env_R = translate_env order evd env in
  let na = Namegen.named_hd env !evd t Anonymous in
- let lams = range (fun k -> (Context.make_annot (prime_name order k na) ERelevance.relevant, None, lift k (prime !evd order k t))) order in
+ let rel = Retyping.relevance_of_type env !evd t in
+ let lams = range (fun k -> (Context.make_annot (prime_name order k na) rel, None, lift k (prime !evd order k t))) order in
  let env_R = push_rel_context (List.map toDecl lams) env_R in
  debug_mode := true;
  debug [`Relation] "output =" env_R !evd res;
@@ -355,7 +356,8 @@ and translate order evd env (t : constr) : constr =
  | Sort _ | Prod (_,_,_) ->
  (* [..., _ : t'', _ : t', _ : t] *)
  let na = Namegen.named_hd env !evd t Anonymous in
- let lams = range (fun k -> (Context.make_annot (prime_name order k na) ERelevance.relevant, lift k (prime !evd order k t))) order in
+ let rel = Retyping.relevance_of_type env !evd t in
+ let lams = range (fun k -> (Context.make_annot (prime_name order k na) rel, lift k (prime !evd order k t))) order in
  compose_lam lams (relation order evd env t)
 
  | App (c,l) ->
@@ -477,7 +479,8 @@ and translate_constant order (evd : Evd.evar_map ref) env cst : constr =
  let etyp = of_constr typ in
  let edef = of_constr def in
  let na = Namegen.named_hd env !evd etyp Anonymous in
- let pred = mkLambda (Context.make_annot na ERelevance.relevant, etyp, substl (range (fun _ -> mkRel 1) order) (relation order evd env etyp)) in
+ let rel = Retyping.relevance_of_type env !evd etyp in
+ let pred = mkLambda (Context.make_annot na rel, etyp, substl (range (fun _ -> mkRel 1) order) (relation order evd env etyp)) in
  let res = translate order evd env edef in
  let uf_opaque_stmt = CoqConstants.eq env evd [| etyp; edef; fold|] in
  let evd', sort = Typing.sort_of env !evd etyp in
@@ -888,7 +891,8 @@ and rewrite_fixpoints order evdr env (depth : int) (fix : fixpoint) source targe
  let env_R =
  if List.exists (fun x -> List.mem x [`Fix]) debug_flag then begin
  let env_R = translate_env order evdr env in
- let rc_order = rev_range (fun k -> Context.make_annot (Name (Id.of_string (Printf.sprintf "rel_%d" k))) ERelevance.relevant, None,
+ let rel = Retyping.relevance_of_type env !evdr typ in
+ let rc_order = rev_range (fun k -> Context.make_annot (Name (Id.of_string (Printf.sprintf "rel_%d" k))) rel, None,
  lift k (prime !evdr order k typ)) order in
  let env_R' = push_rel_context (List.map toDecl rc_order) env_R in
  debug [`Fix] "typ_R =" env_R' !evdr typ_R;