diff options
| -rw-r--r-- | toplevel/assumptions.ml | 4 |
1 files changed, 3 insertions, 1 deletions
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 |