From 3116aeff0cdc51e6801f3e8ae4a6c0533e1a75ac Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 8 Oct 2015 18:06:55 +0200
Subject: Fix #4346 1/2: native casts were not inferring universe constraints.

---
 proofs/redexpr.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'proofs/redexpr.ml')

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index f172bbdd1a..be92f2b04c 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -35,8 +35,7 @@ let cbv_native env sigma c =
     cbv_vm env sigma c
   else
     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
+    Nativenorm.native_norm env sigma c ctyp
 
 let whd_cbn flags env sigma t =
   let (state,_) =
-- 
cgit v1.2.3


From 80bbdf335be5657f5ab33b4aa02e21420d341de2 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sat, 2 Jan 2016 17:11:03 +0100
Subject: Remove some unused functions.

Note: they do not even seem to have a debugging purpose, so better remove
them before they bitrot.
---
 proofs/redexpr.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'proofs/redexpr.ml')

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index be92f2b04c..89ecdb0df2 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -158,8 +158,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
-- 
cgit v1.2.3


From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 20 Jan 2016 17:25:10 +0100
Subject: Update copyright headers.

---
 proofs/redexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/redexpr.ml')

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index be92f2b04c..ea21917ac4 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
-- 
cgit v1.2.3


From 5180ab68819f10949cd41a2458bff877b3ec3204 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 15 Feb 2016 16:45:18 +0100
Subject: Using monotonic types for conversion functions.

---
 proofs/redexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/redexpr.ml')

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 818805a56c..2d886b8e1f 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -194,7 +194,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.
-- 
cgit v1.2.3