diff options
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 1c636275a4..8279c14527 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -186,7 +186,7 @@ let interp_mutual lparams lnamearconstrs finite = let env_params, params = List.fold_left (fun (env, params) (id,t) -> - let p = interp_type sigma env t in + let p = interp_binder sigma env (Name id) t in (Termops.push_rel_assum (Name id,p) env, (Name id,None,p)::params)) (env0,[]) lparams in |