-let signature_of_hypothesis context =
- List.fold_left
- (fun set hyp ->
- match hyp with
- | None -> set
- | Some (_, Cic.Decl t)
- | Some (_, Cic.Def (t, _)) ->
- Constr.UriManagerSet.union set (Constr.constants_of t))
- Constr.UriManagerSet.empty context
+let signature_of_hypothesis context metasenv =
+ let set, _ =
+ List.fold_right
+ (fun hyp (set,current_ctx) ->
+ match hyp with
+ | None -> set, hyp::current_ctx
+ | Some (_, Cic.Decl t) ->
+ Constr.UriManagerSet.union set (Constr.constants_of t),
+ hyp::current_ctx
+ | Some (_, Cic.Def (t, _)) ->
+ try
+ let ty,_ =
+ CicTypeChecker.type_of_aux'
+ metasenv current_ctx t CicUniv.empty_ugraph
+ in
+ let sort,_ =
+ CicTypeChecker.type_of_aux'
+ metasenv current_ctx ty CicUniv.empty_ugraph
+ in
+ match sort with
+ | Cic.Sort Cic.Prop -> set, hyp::current_ctx
+ | _ -> Constr.UriManagerSet.union set (Constr.constants_of t),
+ hyp::current_ctx
+ with
+ | CicTypeChecker.TypeCheckerFailure _ -> set, hyp::current_ctx)
+ context (Constr.UriManagerSet.empty,[])
+ in
+ set
+;;