From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 proofs/redexpr.ml | 30 ++++++++++++++++++++----------
 1 file changed, 20 insertions(+), 10 deletions(-)

(limited to 'proofs/redexpr.ml')

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index ea21917a..72cb05f1 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Term
@@ -17,7 +17,7 @@ open Genredexpr
 open Pattern
 open Reductionops
 open Tacred
-open Closure
+open CClosure
 open RedFlags
 open Libobject
 open Misctypes
@@ -29,17 +29,22 @@ let cbv_vm env sigma c =
     error "vm_compute does not support existential variables.";
   Vnorm.cbv_vm env c ctyp
 
+let warn_native_compute_disabled =
+  CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler"
+  (fun () ->
+   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
-    let () = msg_warning (str "native_compute disabled at configure time; falling back to vm_compute.") in
-    cbv_vm env sigma c
+    (warn_native_compute_disabled ();
+     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,_) =
-    (whd_state_gen true flags env sigma (t,Reductionops.Stack.empty))
+    (whd_state_gen true true flags env sigma (t,Reductionops.Stack.empty))
   in Reductionops.Stack.zip ~refold:true state
 
 let strong_cbn flags =
@@ -141,7 +146,9 @@ let make_flag_constant = function
 let make_flag env f =
   let red = no_red in
   let red = if f.rBeta then red_add red fBETA else red in
-  let red = if f.rIota then red_add red fIOTA else red in
+  let red = if f.rMatch then red_add red fMATCH else red in
+  let red = if f.rFix then red_add red fFIX else red in
+  let red = if f.rCofix then red_add red fCOFIX else red in
   let red = if f.rZeta then red_add red fZETA else red in
   let red =
     if f.rDelta then (* All but rConst *)
@@ -158,8 +165,6 @@ let make_flag env f =
 	  f.rConst red
   in red
 
-let is_reference = function PRef _ | PVar _ -> true | _ -> false
-
 (* table of custom reductino fonctions, not synchronized,
    filled via ML calls to [declare_reduction] *)
 let reduction_tab = ref String.Map.empty
@@ -196,7 +201,7 @@ let out_arg = function
 let out_with_occurrences (occs,c) =
   (Locusops.occurrences_map (List.map out_arg) occs, c)
 
-let e_red f env evm c = evm, f env evm c
+let e_red f = { e_redfun = fun env evm c -> Sigma.here (f env (Sigma.to_evar_map evm) c) evm }
 
 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.
@@ -211,6 +216,11 @@ let contextualize f g = function
       e_red (contextually b (l,c) (fun _ -> h))
   | None -> e_red g
 
+let warn_simpl_unfolding_modifiers =
+  CWarnings.create ~name:"simpl-unfolding-modifiers" ~category:"tactics"
+         (fun () ->
+          Pp.strbrk "The legacy simpl ignores constant unfolding modifiers.")
+
 let reduction_of_red_expr env =
   let make_flag = make_flag env in
   let rec reduction_of_red_expr = function
@@ -223,7 +233,7 @@ let reduction_of_red_expr env =
      let am = if !simplIsCbn then strong_cbn (make_flag f) else simpl in
      let () =
        if not (!simplIsCbn || List.is_empty f.rConst) then
-	 Pp.msg_warning (Pp.strbrk "The legacy simpl does not deal with delta flags.") in
+	 warn_simpl_unfolding_modifiers () in
      (contextualize (if head_style then whd_am else am) am o,DEFAULTcast)
   | Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast)
   | Cbn f ->
-- 
cgit v1.2.3