ncheck works in the current ctx

[helm.git] / helm / software / components / ng_tactics / nTacStatus.ml

diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index 52a45bbd49dd83a2267997f0b9532cf9313753d2..0bb0d846e9fedc5c3b9bc2a7da01f8b3701e66c5 100644 (file)
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -14,7 +14,7 @@
 exception Error of string lazy_t * exn option
 let fail ?exn msg = raise (Error (msg,exn))
 
-let wrap f x = 
+let wrap f x =
   try f x 
   with 
   | MultiPassDisambiguator.DisambiguationError _ 
@@ -152,6 +152,14 @@ let unify status ctx a b =
 ;;
 let unify a b c d = wrap (unify a b c) d;;
 
+let fix_sorts (name,ctx,t) =
+ let f () =
+  let t = NCicUnification.fix_sorts t in
+   name,ctx,t
+ in
+  wrap f ()
+;;
+
 let refine status ctx term expty =
   let status, (nt,_,term) = relocate status ctx term in
   let status, ne, expty = 
@@ -231,8 +239,8 @@ let select_term
     (* we could lift wanted step-by-step *)
     try true, unify status ctx (None, ctx, t) wanted
     with 
-    | NCicUnification.UnificationFailure _ 
-    | NCicUnification.Uncertain _ -> false, status
+    | Error (_, Some (NCicUnification.UnificationFailure _))
+    | Error (_, Some (NCicUnification.Uncertain _)) -> false, status
   in
   let match_term status ctx (wanted : cic_term) t =
     let rec aux ctx (status,already_found) t =