Imported Upstream version 8.5~beta3+dfsg

1 files changed, 13 insertions, 7 deletions

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 1383d755..be92f2b0 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -30,9 +30,12 @@ let cbv_vm env sigma c =
   Vnorm.cbv_vm env c ctyp
 
 let cbv_native env sigma c =
-  let ctyp = Retyping.get_type_of env sigma c in
-  let evars = Nativenorm.evars_of_evar_map sigma in
-  Nativenorm.native_norm env evars c ctyp
+  if Coq_config.no_native_compiler then
+    let () = msg_warning (str "native_compute disabled at configure time; falling back to vm_compute.") in
+    cbv_vm env sigma c
+  else
+    let ctyp = Retyping.get_type_of env sigma c in
+    Nativenorm.native_norm env sigma c ctyp
 
 let whd_cbn flags env sigma t =
   let (state,_) =
@@ -167,18 +170,20 @@ let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction"
 
 let declare_reduction s f =
   if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
-  then error ("There is already a reduction expression of name "^s)
+  then errorlabstrm "Redexpr.declare_reduction"
+    (str "There is already a reduction expression of name " ++ str s)
   else reduction_tab := String.Map.add s f !reduction_tab
 
 let check_custom = function
   | ExtraRedExpr s ->
       if not (String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab)
-      then error ("Reference to undefined reduction expression "^s)
+      then errorlabstrm "Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s)
   |_ -> ()
 
 let decl_red_expr s e =
   if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
-  then error ("There is already a reduction expression of name "^s)
+  then errorlabstrm "Redexpr.decl_red_expr"
+    (str "There is already a reduction expression of name " ++ str s)
   else begin
     check_custom e;
     red_expr_tab := String.Map.add s e !red_expr_tab
@@ -232,7 +237,8 @@ let reduction_of_red_expr env =
       with Not_found ->
 	(try reduction_of_red_expr (String.Map.find s !red_expr_tab)
 	 with Not_found ->
-	   error("unknown user-defined reduction \""^s^"\"")))
+	   errorlabstrm "Redexpr.reduction_of_red_expr"
+             (str "unknown user-defined reduction \"" ++ str s ++ str "\"")))
   | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast)
   | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast)
   in