Ad-hoc management of ? vs out_scope in instantiate. The library passes again,

but there seems to be still more work to do in instantiate.

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 936d1ec8d0c3882e37aa444c3464e16140d26eb3..71b790a26cf3c0e874963ec6ee7b530c57d9d393 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -307,11 +307,30 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
         let t = NCic.Sort (NCic.Type u) in
         move_to_subst n attrs cc t ty metasenv subst  
       else (raise exc)
-  | _, _, NCic.Meta(m,lcm), _ when List.mem_assoc m subst ->
-      (* deref needed for locked metas, maybe should be done outside *)
-      let _,_,bo,_ = NCicUtils.lookup_subst m subst in
-      let bo = NCicSubstitution.subst_meta lcm bo in
-      instantiate rdb test_eq_only metasenv subst context n lc bo swap
+  | kind, ty, NCic.Meta(m,lcm), _ when List.mem_assoc m subst ->
+      let at,ccm,bo,tym = NCicUtils.lookup_subst m subst in
+       if NCicMetaSubst.is_out_scope_tag at then
+        begin
+         (* Case meta vs out-scope *)
+         pp(lazy("4.1"));
+         let ty_t, ccm, kindm = 
+           NCicSubstitution.subst_meta lcm tym, ccm,
+            NCicUntrusted.kind_of_meta at in
+         let lty = NCicSubstitution.subst_meta lc ty in
+         pp (lazy ("On the types: " ^
+           ppterm ~metasenv ~subst ~context lty ^
+           (if test_eq_only then " === " else "=<=") ^
+           ppterm ~metasenv ~subst ~context ty_t)); 
+         let metasenv, subst = 
+           unify rdb test_eq_only metasenv subst context ty_t lty in
+         (*CSC: here I should call kindfy, but it fails since the second
+           meta in in the susbt, not the metasenv! *)
+      (*  let metasenv,t = kindfy exc metasenv subst ccm m lcm ty_t kindm kind in *)
+         delift_to_subst test_eq_only n lc attrs cc t ty context metasenv subst 
+        end
+       else
+        let bo = NCicSubstitution.subst_meta lcm bo in
+        instantiate rdb test_eq_only metasenv subst context n lc bo swap
   | kind, (NCic.Implicit (`Typeof _) as bot),  NCic.Meta(m,lcm), _ ->
       pp(lazy("5"));
       let attrsm, ccm, tym = NCicUtils.lookup_meta m metasenv in