diff options
| author | Matthieu Sozeau | 2014-06-24 18:09:25 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-24 18:53:52 +0200 |
| commit | 0dac8434c9f4190becfd8f169e588fc0270f5397 (patch) | |
| tree | b975900926f62c8289e6eeb570a9c649b119d2de | |
| parent | ff2da62916d9a6bec4aae1a576ce5d396ea9893e (diff) | |
Fix computation of Type argument for Program's fix_proto.
| -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 |