From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 proofs/redexpr.ml | 54 +++++++++++++++++++++++++++++++-----------------------
 1 file changed, 31 insertions(+), 23 deletions(-)

(limited to 'proofs/redexpr.ml')

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 72cb05f1..6fb41193 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Pp
@@ -11,6 +13,7 @@ open CErrors
 open Util
 open Names
 open Term
+open EConstr
 open Declarations
 open Globnames
 open Genredexpr
@@ -24,10 +27,11 @@ open Misctypes
 
 (* call by value normalisation function using the virtual machine *)
 let cbv_vm env sigma c =
-  let ctyp = Retyping.get_type_of env sigma c in
-  if Termops.occur_meta_or_existential c then
-    error "vm_compute does not support existential variables.";
-  Vnorm.cbv_vm env c ctyp
+  if Coq_config.bytecode_compiler then
+    let ctyp = Retyping.get_type_of env sigma c in
+    Vnorm.cbv_vm env sigma c ctyp
+  else
+    compute env sigma c
 
 let warn_native_compute_disabled =
   CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler"
@@ -35,24 +39,25 @@ let warn_native_compute_disabled =
    strbrk "native_compute disabled at configure time; falling back to vm_compute.")
 
 let cbv_native env sigma c =
-  if Coq_config.no_native_compiler then
-    (warn_native_compute_disabled ();
-     cbv_vm env sigma c)
-  else
+  if Coq_config.native_compiler then
     let ctyp = Retyping.get_type_of env sigma c in
     Nativenorm.native_norm env sigma c ctyp
+  else
+    (warn_native_compute_disabled ();
+     cbv_vm env sigma c)
 
 let whd_cbn flags env sigma t =
   let (state,_) =
-    (whd_state_gen true true flags env sigma (t,Reductionops.Stack.empty))
-  in Reductionops.Stack.zip ~refold:true state
+    (whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t,Reductionops.Stack.empty))
+  in
+  Reductionops.Stack.zip ~refold:true sigma state
 
 let strong_cbn flags =
   strong (whd_cbn flags)
 
 let simplIsCbn = ref (false)
 let _ = Goptions.declare_bool_option {
-  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optdepr = false;
   Goptions.optname =
     "Plug the simpl tactic to the new cbn mechanism";
   Goptions.optkey = ["SimplIsCbn"];
@@ -73,7 +78,7 @@ let set_strategy_one ref l  =
         let cb = Global.lookup_constant sp in
 	(match cb.const_body with
 	  | OpaqueDef _ ->
-            errorlabstrm "set_transparent_const"
+            user_err ~hdr:"set_transparent_const"
               (str "Cannot make" ++ spc () ++
 		 Nametab.pr_global_env Id.Set.empty (ConstRef sp) ++
 		 spc () ++ str "transparent because it was declared opaque.");
@@ -175,19 +180,19 @@ 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 errorlabstrm "Redexpr.declare_reduction"
+  then user_err ~hdr:"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 errorlabstrm "Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s)
+      then user_err ~hdr:"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 errorlabstrm "Redexpr.decl_red_expr"
+  then user_err ~hdr:"Redexpr.decl_red_expr"
     (str "There is already a reduction expression of name " ++ str s)
   else begin
     check_custom e;
@@ -195,13 +200,13 @@ let decl_red_expr s e =
   end
 
 let out_arg = function
-  | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable")
+  | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.")
   | ArgArg x -> x
 
 let out_with_occurrences (occs,c) =
   (Locusops.occurrences_map (List.map out_arg) occs, c)
 
-let e_red f = { e_redfun = fun env evm c -> Sigma.here (f env (Sigma.to_evar_map evm) c) evm }
+let e_red f env evm c = evm, f env evm c
 
 let head_style = false (* Turn to true to have a semantics where simpl
    only reduce at the head when an evaluable reference is given, e.g.
@@ -247,16 +252,19 @@ let reduction_of_red_expr env =
       with Not_found ->
 	(try reduction_of_red_expr (String.Map.find s !red_expr_tab)
 	 with Not_found ->
-	   errorlabstrm "Redexpr.reduction_of_red_expr"
+	   user_err ~hdr:"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
     reduction_of_red_expr
 
+let subst_mps subst c =
+  EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c))
+
 let subst_red_expr subs =
   Miscops.map_red_expr_gen
-    (Mod_subst.subst_mps subs)
+    (subst_mps subs)
     (Mod_subst.subst_evaluable_reference subs)
     (Patternops.subst_pattern subs)
 
-- 
cgit v1.2.3