Wrong context (again!)

[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 6664a5b9781cf0b06bb465c78f9f017558d6c522..e2aabb31cddd76a68c301841dad7746827516adf 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -42,6 +42,8 @@ let exp_implicit ~localise metasenv context expty t =
   | `Closed -> NCicMetaSubst.mk_meta metasenv [] (foo `Term)
   | `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type)
   | `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term)
+  | `Tagged s ->
+      NCicMetaSubst.mk_meta ~attrs:[`Name s] metasenv context (foo `Term)
   | `Vector ->
       raise (RefineFailure (lazy (localise t, "A vector of implicit terms " ^
        "can only be used in argument position")))
@@ -240,7 +242,8 @@ let rec typeof rdb
          | Some x -> 
              let m, s, x = 
                NCicUnification.delift_type_wrt_terms 
-                 rdb metasenv subst context x [t]
+                rdb metasenv subst context1 (NCicSubstitution.lift 1 x)
+                [NCicSubstitution.lift 1 t]
              in
                m, s, Some x
        in
@@ -308,7 +311,7 @@ let rec typeof rdb
       let metasenv =
        List.filter (function (j,_) -> j <> metanoouttype) metasenv in
       let subst =
-       (metanoouttype,(Some "outtype",context,outtype,metaoutsort))::subst in
+       (metanoouttype,([`Name "outtype"],context,outtype,metaoutsort))::subst in
       let outtype = newouttype in
 
       (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)