diff options
| -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 1f9d725b83..faa4b12dfd 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -935,7 +935,7 @@ let interp_recursive isfix fixl notations = List.fold_left2 (fun env' id t -> if Flags.is_program_mode () then - let sort = Retyping.get_type_of env !evdref t in + let sort = Evarutil.evd_comb1 (Typing.e_type_of ~refresh:true env) evdref t in let fixprot = try let app = mkApp (delayed_force fix_proto, [|sort; t|]) in |