...

[helm.git] / helm / software / components / ng_refiner / check.ml

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 3a155329e679ba235f2c5da77987ae69455b96c4..851cda9d2f3fc833853005c0af386cab1cc47311 100644 (file)
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -198,17 +198,28 @@ let _ =
       let u = OCic2NCic.nuri_of_ouri u in
       indent := 0;
       match NCicLibrary.get_obj u with
-      | _,_,_,_,NCic.Constant (_,_,Some bo, ty, _) ->
+      | _,_,_,_,NCic.Constant (_,_,_, ty, _) ->
           let rec intros = function
             | NCic.Prod (name, s, t) ->
                 let ctx, t = intros t in
                 ctx @ [(name, (NCic.Decl s))] , t
             | t -> [], t
           in
+          let rec perforate ctx menv = function
+            | NCic.Appl (NCic.Const (NReference.Ref (u,_))::ty::_)
+              when NUri.string_of_uri u = "cic:/matita/tests/hole.con" ->
+                NCicMetaSubst.mk_meta menv ctx ty
+            | t -> 
+                NCicUntrusted.map_term_fold_a
+                 (fun e ctx -> e::ctx) ctx perforate menv t
+          in
           let ctx, ity = intros ty in
+          let menv, pty = perforate [] [] ty in
+(*
           let sty, menv, _ = 
             NCicMetaSubst.saturate ~delta:max_int [] ctx ty 0
           in
+*)
           let ctx, ty = intros ty in
           let whd ty =
             match ty with
@@ -225,7 +236,7 @@ let _ =
           let metasenv, subst = 
             try 
 (*                     prerr_endline ("INIZIO: " ^ NUri.string_of_uri u); *)
-              NCicUnification.unify menv [] ctx ity (whd sty) 
+              NCicUnification.unify menv [] ctx ity sty
             with
             | NCicUnification.Uncertain msg 
             | NCicUnification.UnificationFailure msg