better pps

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 5e68057bb21f6559e2424ed589a8f71cd1cfc129..bb423690b177a2865aae6b19914822e555ffa61f 100644 (file)
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -265,53 +265,54 @@ let _ =
                  (NCicPp.ppterm ~metasenv:metasenv ~subst:[] ~context:ctx ity)
                  (NCicPp.ppterm ~metasenv:metasenv ~subst:[] ~context:ctx sty));
 *)
                  (NCicPp.ppterm ~metasenv:metasenv ~subst:[] ~context:ctx ity)
                  (NCicPp.ppterm ~metasenv:metasenv ~subst:[] ~context:ctx sty));
 *)

-          let metasenv, subst, bo, infty = 
-            let bo = curryfy [] bo in
-            try NCicRefiner.typeof [] [] [] bo None
-            with
-            | NCicRefiner.RefineFailure msg 
-            | NCicRefiner.Uncertain msg ->
-               let _, msg = Lazy.force msg in
-               prerr_endline msg;
-               assert false
-          in
-          prerr_endline "XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX";
-          let metasenv, subst = 
-            try 
-              NCicUnification.unify metasenv subst [] infty ty
-            with
-            | NCicUnification.Uncertain msg 
-            | NCicUnification.UnificationFailure msg 
-            | NCicMetaSubst.MetaSubstFailure msg ->
-                prerr_endline (Lazy.force msg); 
-                metasenv, subst
-            | Sys.Break -> metasenv, subst
-          in
-          if (NCicReduction.are_convertible ~subst [] infty ty)
-          then
-            prerr_endline ("OK: " ^ NUri.string_of_uri u)
-          else
-            (
-          let ctx = [] in
-          let right = infty in
-          let left = ty in
-                    
-                    prerr_endline ("FAIL: " ^ NUri.string_of_uri u);
-                prerr_endline 
-                 (Printf.sprintf 
-                   ("\t\tRESULT OF UNIF\n\nsubst:\n%s\nmetasenv:\n%s\n" ^^ 
-                   "context:\n%s\nTERMS NO SUBST:\n%s\n==\n%s\n"^^
-                   "TERMS:\n%s\n==\n%s\n")
-                 (NCicPp.ppsubst ~metasenv subst)
-                 (NCicPp.ppmetasenv ~subst metasenv)
-                 (NCicPp.ppcontext ~metasenv ~subst ctx)
-                 (NCicPp.ppterm ~metasenv ~subst:[] ~context:ctx left)
-                 (NCicPp.ppterm ~metasenv ~subst:[] ~context:ctx right)
-                 (NCicPp.ppterm ~metasenv ~subst ~context:ctx left)
-                 (NCicPp.ppterm ~metasenv ~subst ~context:ctx right) ))
-          (*let inferred_ty = 
-            NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] bo
-          in*)
+          prerr_endline ("start: " ^ NUri.string_of_uri u);
+          let bo = curryfy [] bo in
+          (try 
+            let metasenv, subst, bo, infty = 
+              NCicRefiner.typeof [] [] [] bo None
+            in
+            let metasenv, subst = 
+              try 
+                NCicUnification.unify metasenv subst [] infty ty
+              with
+              | NCicUnification.Uncertain msg 
+              | NCicUnification.UnificationFailure msg 
+              | NCicMetaSubst.MetaSubstFailure msg ->
+                  prerr_endline (Lazy.force msg); 
+                  metasenv, subst
+              | Sys.Break -> metasenv, subst
+            in
+            if (NCicReduction.are_convertible ~subst [] infty ty)
+            then
+              prerr_endline ("OK: " ^ NUri.string_of_uri u)
+            else
+              (
+            let ctx = [] in
+            let right = infty in
+            let left = ty in
+                      
+                      prerr_endline ("FAIL: " ^ NUri.string_of_uri u);
+                  prerr_endline 
+                   (Printf.sprintf 
+                     ("\t\tRESULT OF UNIF\n\nsubst:\n%s\nmetasenv:\n%s\n" ^^ 
+                     "context:\n%s\nTERMS NO SUBST:\n%s\n==\n%s\n"^^
+                     "TERMS:\n%s\n==\n%s\n")
+                   (NCicPp.ppsubst ~metasenv subst)
+                   (NCicPp.ppmetasenv ~subst metasenv)
+                   (NCicPp.ppcontext ~metasenv ~subst ctx)
+                   (NCicPp.ppterm ~metasenv ~subst:[] ~context:ctx left)
+                   (NCicPp.ppterm ~metasenv ~subst:[] ~context:ctx right)
+                   (NCicPp.ppterm ~metasenv ~subst ~context:ctx left)
+                   (NCicPp.ppterm ~metasenv ~subst ~context:ctx right) ))
+            (*let inferred_ty = 
+              NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] bo
+            in*)
+          with
+          | NCicRefiner.RefineFailure msg 
+          | NCicRefiner.Uncertain msg ->
+             let _, msg = Lazy.force msg in
+             prerr_endline msg;
+             prerr_endline ("FAIL: " ^ NUri.string_of_uri u))

       | _ -> ())
     alluris;
 ;;
       | _ -> ())
     alluris;
 ;;