From 4944b5e72c0f4bfcf1ae140f810d8666dac3cf60 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 15 May 2015 14:26:35 +0200
Subject: Make Coercion.inh_app_fun respect its specification.

It enhances bug #3527, as instead of raising an anomaly "Uncaught
exception Coercion.NoCoercion(_)", it now fails with a typing error.
---
 pretyping/coercion.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index f5135f5c60..6765ca130b 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -378,7 +378,8 @@ let inh_app_fun env evd j =
       	try let t,p =
 	  lookup_path_to_fun_from env evd j.uj_type in
 	    apply_coercion env evd p j t
-	with Not_found | NoCoercion when Flags.is_program_mode () ->
+	with Not_found | NoCoercion ->
+          if Flags.is_program_mode () then
 	  try
 	    let evdref = ref evd in
 	    let coercef, t = mu env evdref t in
@@ -386,6 +387,7 @@ let inh_app_fun env evd j =
 	      (!evdref, res)
 	  with NoSubtacCoercion | NoCoercion ->
 	    (evd,j)
+          else (evd, j)
 
 let inh_app_fun resolve_tc env evd j =
   try inh_app_fun env evd j
-- 
cgit v1.2.3


From 5a52a74592496353d562d9f3e958fb59ab585531 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 19 May 2015 19:36:31 +0200
Subject: Adding an extensible global state to evarmaps.

Evars already had their own extensible state, but adding it globally allows
to write out extensible state-passing code in e.g. plugins. The additional
data is hopefully transparently preserved by the code out there. Trespassers
ought to be prosecuted.
---
 pretyping/evd.ml  |  9 +++++++++
 pretyping/evd.mli | 13 +++++++++++++
 2 files changed, 22 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index f414d71dc1..18e668d288 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -564,6 +564,7 @@ type evar_map = {
                                              name) of the evar which
                                              will be instantiated with
                                              a term containing [e]. *)
+  extras : Store.t;
 }
 
 (*** Lifting primitive from Evar.Map. ***)
@@ -745,6 +746,7 @@ let empty = {
   evar_names = (EvMap.empty,Idmap.empty); (* id<->key for undefined evars *)
   future_goals = [];
   principal_future_goal = None;
+  extras = Store.empty;
 }
 
 let from_env ?ctx e = 
@@ -1320,6 +1322,7 @@ let set_metas evd metas = {
   evar_names = evd.evar_names;
   future_goals = evd.future_goals;
   principal_future_goal = evd.principal_future_goal;
+  extras = Store.empty;
 }
 
 let meta_list evd = metamap_to_list evd.metas
@@ -1468,6 +1471,12 @@ let dependent_evar_ident ev evd =
   | (_,Evar_kinds.VarInstance id) -> id
   | _ -> anomaly (str "Not an evar resulting of a dependent binding")
 
+(**********************************************************)
+(* Extra data *)
+
+let get_extra_data evd = evd.extras
+let set_extra_data extras evd = { evd with extras }
+
 (*******************************************************************)
 
 type pending = (* before: *) evar_map * (* after: *) evar_map
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index eca6d60ad5..15ce979d0c 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -310,6 +310,19 @@ val add_universe_constraints : evar_map -> Universes.universe_constraints -> eva
     @raises UniversesDiffer in case a first-order unification fails.
     @raises UniverseInconsistency
 *)
+
+(** {5 Extra data}
+
+  Evar maps can contain arbitrary data, allowing to use an extensible state.
+  As evar maps are theoretically used in a strict state-passing style, such
+  additional data should be passed along transparently. Some old and bug-prone
+  code tends to drop them nonetheless, so you should keep cautious.
+
+*)
+
+val get_extra_data : evar_map -> Store.t
+val set_extra_data : Store.t -> evar_map -> evar_map
+
 (** {5 Enriching with evar maps} *)
 
 type 'a sigma = {
-- 
cgit v1.2.3


From 866c41b9720413e00194ba7addb9c4277e114890 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 27 May 2015 11:43:11 +0200
Subject: Fix bug #4159 Some asynchronous constraints between initial universes
 and the ones at the end of a proof were forgotten. Also add a message to
 print universes indicating if all the constraints are processed already or
 not.

---
 pretyping/evd.ml  | 16 +++++++++++++++-
 pretyping/evd.mli |  2 +-
 2 files changed, 16 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 18e668d288..fe96aa347d 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -330,9 +330,23 @@ let union_evar_universe_context ctx ctx' =
 
 type 'a in_evar_universe_context = 'a * evar_universe_context
 
-let evar_universe_context_set ctx = ctx.uctx_local
+let evar_universe_context_set diff ctx =
+  let initctx = ctx.uctx_local in
+  let cstrs =
+    Univ.LSet.fold
+      (fun l cstrs ->
+       try
+	 match Univ.LMap.find l ctx.uctx_univ_variables with
+	 | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs
+	 | None -> cstrs
+       with Not_found -> cstrs)
+      (Univ.Instance.levels (Univ.UContext.instance diff)) Univ.Constraint.empty
+  in
+    Univ.ContextSet.add_constraints cstrs initctx 
+		      
 let evar_universe_context_constraints ctx = snd ctx.uctx_local
 let evar_context_universe_context ctx = Univ.ContextSet.to_context ctx.uctx_local
+    
 let evar_universe_context_of ctx = { empty_evar_universe_context with uctx_local = ctx }
 let evar_universe_context_subst ctx = ctx.uctx_univ_variables
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 15ce979d0c..f2d8a83350 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -475,7 +475,7 @@ val univ_flexible_alg : rigid
 
 type 'a in_evar_universe_context = 'a * evar_universe_context
 
-val evar_universe_context_set : evar_universe_context -> Univ.universe_context_set
+val evar_universe_context_set : Univ.universe_context -> evar_universe_context -> Univ.universe_context_set
 val evar_universe_context_constraints : evar_universe_context -> Univ.constraints
 val evar_context_universe_context : evar_universe_context -> Univ.universe_context
 val evar_universe_context_of : Univ.universe_context_set -> evar_universe_context
-- 
cgit v1.2.3


From 83188dacc43df02245d13810d08cc63b7a5633ed Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 28 May 2015 14:13:12 +0200
Subject: Fixup for 866c41b

---
 pretyping/evd.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index fe96aa347d..60b1da7049 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -339,7 +339,7 @@ let evar_universe_context_set diff ctx =
 	 match Univ.LMap.find l ctx.uctx_univ_variables with
 	 | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs
 	 | None -> cstrs
-       with Not_found -> cstrs)
+       with Not_found | Option.IsNone -> cstrs)
       (Univ.Instance.levels (Univ.UContext.instance diff)) Univ.Constraint.empty
   in
     Univ.ContextSet.add_constraints cstrs initctx 
-- 
cgit v1.2.3