diff options
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 6a3d9a11a..e3a299340 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -316,10 +316,10 @@ let interp_mutual_inductive (paramsl,indl) notations finite = let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env_params evd in let sigma = evd in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in - let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in + let ctx_params = Context.map_rel_context (nf_evar sigma) ctx_params in let arities = List.map (nf_evar sigma) arities in List.iter (check_evars env_params Evd.empty evd) arities; - Sign.iter_rel_context (check_evars env0 Evd.empty evd) ctx_params; + Context.iter_rel_context (check_evars env0 Evd.empty evd) ctx_params; List.iter (fun (_,ctyps,_) -> List.iter (check_evars env_ar_params Evd.empty evd) ctyps) constructors; |