From 840cefca77a48ad68641539cd26d8d2e8c9dc031 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 17 Dec 2015 20:32:09 +0100
Subject: (Partial) fix for bug #4453: raise an error instead of an anomaly.

---
 pretyping/typing.ml | 18 +++++++++++++++---
 1 file changed, 15 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index fb5927dbf7..db980e455a 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -144,8 +144,13 @@ let e_judge_of_cast env evdref cj k tj =
   { uj_val = mkCast (cj.uj_val, k, expected_type);
     uj_type = expected_type }
 
-(* The typing machine without information, without universes but with
-   existential variables. *)
+let enrich_env env evdref =
+  let penv = Environ.pre_env env in
+  let penv' = Pre_env.({ penv with env_stratification =
+    { penv.env_stratification with env_universes = Evd.universes !evdref } }) in
+  Environ.env_of_pre_env penv'
+			  
+(* The typing machine with universes and existential variables. *)
 
 (* cstr must be in n.f. w.r.t. evars and execute returns a judgement
    where both the term and type are in n.f. *)
@@ -264,6 +269,7 @@ and execute_recdef env evdref (names,lar,vdef) =
 and execute_array env evdref = Array.map (execute env evdref)
 
 let check env evdref c t =
+  let env = enrich_env env evdref in
   let j = execute env evdref c in
   if not (Evarconv.e_cumul env evdref j.uj_type t) then
     error_actual_type env j (nf_evar !evdref t)
@@ -271,12 +277,15 @@ let check env evdref c t =
 (* Type of a constr *)
 
 let unsafe_type_of env evd c =
-  let j = execute env (ref evd) c in
+  let evdref = ref evd in
+  let env = enrich_env env evdref in
+  let j = execute env evdref c in
     j.uj_type
 
 (* Sort of a type *)
 
 let sort_of env evdref c =
+  let env = enrich_env env evdref in
   let j = execute env evdref c in
   let a = e_type_judgment env evdref j in
   a.utj_type
@@ -285,6 +294,7 @@ let sort_of env evdref c =
 
 let type_of ?(refresh=false) env evd c =
   let evdref = ref evd in
+  let env = enrich_env env evdref in
   let j = execute env evdref c in
   (* side-effect on evdref *)
     if refresh then
@@ -292,6 +302,7 @@ let type_of ?(refresh=false) env evd c =
     else !evdref, j.uj_type
 
 let e_type_of ?(refresh=false) env evdref c =
+  let env = enrich_env env evdref in
   let j = execute env evdref c in
   (* side-effect on evdref *)
     if refresh then
@@ -301,6 +312,7 @@ let e_type_of ?(refresh=false) env evdref c =
     else j.uj_type
 
 let solve_evars env evdref c =
+  let env = enrich_env env evdref in
   let c = (execute env evdref c).uj_val in
   (* side-effect on evdref *)
   nf_evar !evdref c
-- 
cgit v1.2.3


From b2eaecf0e748e3c286e1ef337f72cee6d3475162 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 Dec 2015 02:48:45 +0100
Subject: Fixing bug #4462: unshelve: Anomaly: Uncaught exception Not_found.

The rewrite tactic was causing an evar leak because of the use of the
Evd.remove primitive. This function did not modify the future goals of
the evarmap to remove the considered evar and thus maintained dangling
evars in there, causing the anomaly.
---
 pretyping/evd.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index c9b9f34414..8edc7a17c6 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -658,7 +658,12 @@ let add d e i = match i.evar_body with
 let remove d e =
   let undf_evars = EvMap.remove e d.undf_evars in
   let defn_evars = EvMap.remove e d.defn_evars in
-  { d with undf_evars; defn_evars; }
+  let principal_future_goal = match d.principal_future_goal with
+  | None -> None
+  | Some e' -> if Evar.equal e e' then None else d.principal_future_goal
+  in
+  let future_goals = List.filter (fun e' -> not (Evar.equal e e')) d.future_goals in
+  { d with undf_evars; defn_evars; principal_future_goal; future_goals }
 
 let find d e =
   try EvMap.find e d.undf_evars
-- 
cgit v1.2.3