diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/globEnv.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml index fad41614b4..e458d030cb 100644 --- a/pretyping/globEnv.ml +++ b/pretyping/globEnv.ml @@ -42,7 +42,7 @@ let make ~hypnaming env sigma lvar = let get_extra env sigma = let avoid = Environ.ids_of_named_context_val (Environ.named_context_val env) in Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context ~hypnaming sigma d acc) - (rel_context env) ~init:(empty_csubst, avoid, named_context env) in + (rel_context env) ~init:(empty_csubst, avoid, named_context_val env) in { static_env = env; renamed_env = env; @@ -98,10 +98,9 @@ let new_evar env sigma ?src ?naming typ = let open Context.Named.Declaration in let inst_vars = List.map (get_id %> mkVar) (named_context env.renamed_env) in let inst_rels = List.rev (rel_list 0 (nb_rel env.renamed_env)) in - let (subst, _, nc) = Lazy.force env.extra in + let (subst, _, sign) = Lazy.force env.extra in let typ' = csubst_subst subst typ in let instance = inst_rels @ inst_vars in - let sign = val_of_named_context nc in new_evar_instance sign sigma typ' ?src ?naming instance let new_type_evar env sigma ~src = |