NCicRefiner.force_to_sort implemented on top of NCicUnification.sortfy.

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 415afdc1de2773129b8f9156758e6ab2cf6031fa..784ceeea88e7a2bc358ac2977ae72685495fdebb 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -453,29 +453,21 @@ and try_coercions rdb
         rdb metasenv subst context infty expty)
 
 and force_to_sort rdb metasenv subst context t orig_t localise ty =
-  match NCicReduction.whd ~subst context ty with
-  | C.Meta (_,(0,(C.Irl 0 | C.Ctx []))) as ty -> 
-     metasenv, subst, t, ty
-  | C.Meta (_i,(_,(C.Irl 0 | C.Ctx []))) -> assert false (*CSC: ???
-     metasenv, subst, t, C.Meta(i,(0,C.Irl 0)) *)
-  | C.Meta (i,(_,lc)) ->
-     let len = match lc with C.Irl len->len | C.Ctx l->List.length l in
-     let metasenv, subst, newmeta, _ = 
-       if len > 0 then
-         NCicMetaSubst.restrict metasenv subst i (HExtlib.list_seq 1 (len+1))
-       else metasenv, subst, i, []
-     in
-     metasenv, subst, t, C.Meta (newmeta,(0,C.Irl 0))
-  | C.Sort _ as ty -> metasenv, subst, t, ty 
-  | ty -> 
-      try_coercions rdb ~localise metasenv subst context
-        t orig_t ty (NCic.Sort (NCic.Type 
-          (match NCicEnvironment.get_universes () with
-           | x::_ -> x 
-           | _ -> assert false))) false 
-         (Uncertain (lazy (localise orig_t, 
-         "The type of " ^ NCicPp.ppterm ~metasenv ~subst ~context t
-         ^ " is not a sort: " ^ NCicPp.ppterm ~metasenv ~subst ~context ty)))
+  try 
+    let metasenv, subst, ty = 
+      NCicUnification.sortfy (Failure "sortfy") metasenv subst context ty in
+      metasenv, subst, t, ty
+  with
+      Failure _ -> 
+        let ty = NCicReduction.whd ~subst context ty in
+          try_coercions rdb ~localise metasenv subst context
+            t orig_t ty (NCic.Sort (NCic.Type 
+              (match NCicEnvironment.get_universes () with
+               | x::_ -> x 
+               | _ -> assert false))) false 
+             (Uncertain (lazy (localise orig_t, 
+             "The type of " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^
+             " is not a sort: " ^ NCicPp.ppterm ~metasenv ~subst ~context ty)))
 
 and sort_of_prod 
   localise metasenv subst context orig_s orig_t (name,s) t (t1, t2) 

diff --git a/helm/software/components/ng_refiner/nCicUnification.mli b/helm/software/components/ng_refiner/nCicUnification.mli
index fef24b2d5cad3b75c5da16b3356e6194ee56c861..954f56e58ee86a895acdd0b074cab1525cfcc492 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.mli
+++ b/helm/software/components/ng_refiner/nCicUnification.mli
@@ -37,5 +37,11 @@ val delift_type_wrt_terms:
   NCic.term -> NCic.term list -> 
    NCic.metasenv * NCic.substitution * NCic.term
 
+val sortfy :
+    exn ->
+    NCic.metasenv ->
+    NCic.substitution ->
+    NCic.context ->
+    NCic.term -> NCic.metasenv * NCic.substitution * NCic.term
 
 val debug : bool ref