From 7dd0c2875b4986d5bfb7615f9cd0c145b6609fe3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 2 Jul 2015 09:24:42 +0200
Subject: Fix loop in assumptions  (Close: #4275)

---
 toplevel/assumptions.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml
index fff7e2e21e..a11653a43b 100644
--- a/toplevel/assumptions.ml
+++ b/toplevel/assumptions.ml
@@ -164,7 +164,8 @@ let rec traverse current ctx accu t = match kind_of_term t with
         let body () = Global.body_of_constant_body (lookup_constant kn) in
         traverse_object
           ~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn)
-    | _ -> Termops.fold_constr_with_full_binders push (traverse current) ctx accu t 
+    | _ ->
+        Termops.fold_constr_with_full_binders push (traverse current) ctx accu t
     end
 | _ -> Termops.fold_constr_with_full_binders push (traverse current) ctx accu t
 
@@ -182,6 +183,7 @@ and traverse_object ?inhabits (curr, data, ax2ty) body obj =
           with Not_found -> Refmap.add obj [ty] ax2ty in
         data, ax2ty
     | Some body ->
+      if already_in then data, ax2ty else
       let contents,data,ax2ty =
         traverse (label_of obj) [] (Refset.empty,data,ax2ty) body in
       Refmap.add obj contents data, ax2ty
-- 
cgit v1.2.3