From 164c6861860e6b52818c031f901ffeff91fca16a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 26 Jan 2016 16:56:33 +0100
Subject: Imported Upstream version 8.5

---
 pretyping/evarsolve.ml | 22 +++++++++++++++-------
 1 file changed, 15 insertions(+), 7 deletions(-)

(limited to 'pretyping/evarsolve.ml')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 35bc1de5..3bf6f376 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.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        *)
@@ -47,7 +47,7 @@ let refresh_level evd s =
   | None -> true
   | Some l -> not (Evd.is_flexible_level evd l)
 
-let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
+let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) pbty env evd t =
   let evdref = ref evd in
   let modified = ref false in
   let rec refresh status dir t = 
@@ -98,7 +98,7 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
     if isArity t then
       (match pbty with
       | None -> t
-      | Some dir -> refresh univ_rigid dir t)
+      | Some dir -> refresh status dir t)
     else (refresh_term_evars false true t; t)
   in
     if !modified then !evdref, t' else !evdref, t
@@ -609,7 +609,8 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
       let id = next_name_away na avoid in
       let evd,t_in_sign =
         let s = Retyping.get_sort_of env evd t_in_env in
-        let evd,ty_t_in_sign = refresh_universes ~inferred:true (Some false) env evd (mkSort s) in
+        let evd,ty_t_in_sign = refresh_universes
+	 ~status:univ_flexible (Some false) env evd (mkSort s) in
         define_evar_from_virtual_equation define_fun env evd src t_in_env
           ty_t_in_sign sign filter inst_in_env in
       let evd,b_in_sign = match b with
@@ -627,7 +628,8 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
   in
   let evd,ev2ty_in_sign =
     let s = Retyping.get_sort_of env evd ty_in_env in
-    let evd,ty_t_in_sign = refresh_universes ~inferred:true (Some false) env evd (mkSort s) in
+    let evd,ty_t_in_sign = refresh_universes
+     ~status:univ_flexible (Some false) env evd (mkSort s) in
     define_evar_from_virtual_equation define_fun env evd src ty_in_env
       ty_t_in_sign sign2 filter2 inst2_in_env in
   let evd,ev2_in_sign =
@@ -1284,10 +1286,16 @@ let solve_candidates conv_algo env evd (evk,argsv) rhs =
       | l -> evd
 
 let occur_evar_upto_types sigma n c =
+  let seen = ref Evar.Set.empty in
   let rec occur_rec c = match kind_of_term c with
     | Evar (sp,_) when Evar.equal sp n -> raise Occur
-    | Evar e -> Option.iter occur_rec (existential_opt_value sigma e);
-		occur_rec (existential_type sigma e)
+    | Evar (sp,args as e) ->
+       if Evar.Set.mem sp !seen then
+         Array.iter occur_rec args
+       else (
+         seen := Evar.Set.add sp !seen;
+	 Option.iter occur_rec (existential_opt_value sigma e);
+	 occur_rec (existential_type sigma e))
     | _ -> iter_constr occur_rec c
   in
   try occur_rec c; false with Occur -> true
-- 
cgit v1.2.3