new tactics are almost ready

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

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 1cd2e54b96614a37ae097022799f109a964d7765..dd03356c4845fb78ad02fd3c5a42e10b5aea20c9 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -153,7 +153,11 @@ let rec typeof hdb
          let _,_,_,ty = NCicUtils.lookup_subst n subst in ty 
         with NCicUtils.Subst_not_found _ -> try
          let _,_,ty = NCicUtils.lookup_meta n metasenv in 
-         match ty with C.Implicit _ -> assert false | _ -> ty 
+         match ty with C.Implicit _ -> 
+                 prerr_endline (string_of_int n);
+                 prerr_endline (NCicPp.ppmetasenv ~subst metasenv);
+                 prerr_endline (NCicPp.ppsubst ~metasenv subst);
+                 assert false | _ -> ty 
         with NCicUtils.Meta_not_found _ ->
          raise (AssertFailure (lazy (Printf.sprintf
           "%s not found" (NCicPp.ppterm ~subst ~metasenv ~context t))))