From 0dac8434c9f4190becfd8f169e588fc0270f5397 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 24 Jun 2014 18:09:25 +0200
Subject: Fix computation of Type argument for Program's fix_proto.

---
 toplevel/command.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3