-let whole_statement_universe =
- ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" ;
- "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" ;
- "http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis" ;
- "http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis"]
-;;
-
-let only_conclusion_universe =
- ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" ;
- "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"]
-;;
-
-let refine_constraints (constr_obj, constr_rel, constr_sort) =
+let refine_constraints ((constr_obj:T.r_obj list), (constr_rel:T.r_rel list), (constr_sort:T.r_sort list)) =