From 4ff2055cabd4ac273b7222f6cf21aedbff5c022d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 15 Oct 2008 22:32:03 +0000
Subject: [PATCH] ...

---
 helm/software/components/ng_refiner/check.ml | 38 ++++++++++++--------
 1 file changed, 23 insertions(+), 15 deletions(-)

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 7fe8cf366..3b951bec2 100644
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -205,14 +205,14 @@ let _ =
                 ctx @ [(name, (NCic.Decl s))] , t
             | t -> [], t
           in
-          let rec perforate ctx menv = function
+          let rec perforate ctx metasenv = function
             | NCic.Appl (NCic.Const (NReference.Ref (u,_))::ty::_)
               when NUri.string_of_uri u = "cic:/matita/tests/hole.con" ->
-                let menv, ty =  perforate ctx menv ty in
-                let a,b,_ = NCicMetaSubst.mk_meta menv ctx (`WithType ty) in a,b
+                let metasenv, ty =  perforate ctx metasenv ty in
+                let a,b,_ = NCicMetaSubst.mk_meta metasenv ctx (`WithType ty) in a,b
             | t -> 
                 NCicUntrusted.map_term_fold_a
-                 (fun e ctx -> e::ctx) ctx perforate menv t
+                 (fun e ctx -> e::ctx) ctx perforate metasenv t
           in
           let rec curryfy ctx = function
             | NCic.Lambda (name, s, tgt) ->
@@ -224,10 +224,10 @@ let _ =
           in
 (*
           let ctx, pty = intros ty in
-          let menv, pty = perforate ctx [] pty in
+          let metasenv, pty = perforate ctx [] pty in
 *)
 (*
-          let sty, menv, _ = 
+          let sty, metasenv, _ = 
             NCicMetaSubst.saturate ~delta:max_int [] ctx ty 0
           in
 *)
@@ -251,22 +251,29 @@ let _ =
 (*
                 prerr_endline 
                  (Printf.sprintf "%s == %s"
-                 (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx ity)
-                 (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx sty));
+                 (NCicPp.ppterm ~metasenv:metasenv ~subst:[] ~context:ctx ity)
+                 (NCicPp.ppterm ~metasenv:metasenv ~subst:[] ~context:ctx sty));
 *)
-          let menv, subst, bo, infty = 
-            NCicRefiner.typeof [] [] [] (curryfy [] bo) None
+          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
           let metasenv, subst = 
             try 
-              NCicUnification.unify menv subst [] infty ty
+              NCicUnification.unify metasenv subst [] infty ty
             with
             | NCicUnification.Uncertain msg 
             | NCicUnification.UnificationFailure msg 
             | NCicMetaSubst.MetaSubstFailure msg ->
                 prerr_endline (Lazy.force msg); 
-                [], []
-            | Sys.Break -> [],[]
+                metasenv, subst
+            | Sys.Break -> metasenv, subst
           in
           if (NCicReduction.are_convertible ~subst [] infty ty)
           then
@@ -280,8 +287,9 @@ let _ =
                     prerr_endline ("FAIL: " ^ NUri.string_of_uri u);
                 prerr_endline 
                  (Printf.sprintf 
-                   ("\t\tRESULT OF UNIF\n\nsubst:\n%s\nmenv:\n%s\n" ^^ 
-                   "context:\n%s\n%s == %s\n%s == %s\n")
+                   ("\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)
-- 
2.39.2