- if tooflex clause then (print (lazy "pruning tooflex"); s)
- else P.forward_infer_step (P.replace_bag s bag) clause 0
- else (debug (lazy "not eq"); s)
+ if tooflex clause then (debug (lazy "pruning tooflex"); s,None)
+ else
+ P.forward_infer_step (P.replace_bag s bag) clause 0, Some clause
+ else (debug (lazy "not eq"); s,None)
+;;
+
+let forward_infer_step status metasenv subst context s t ty =
+ fst (forward_infer_step0 status metasenv subst context s t ty)