X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=58036784f634e8e8427f3c86d4987ac0fce35d0b;hb=86dbca4f0bfda375bdf036ec5ce3bf44678415f2;hp=a1ce81470d36d66dd4ae4fe99ef5c772fec95b4d;hpb=8b1a49bbee9eea86eb74c040defe701370ca5893;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index a1ce81470..58036784f 100644
--- 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")))
@@ -308,7 +310,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] *)
@@ -380,15 +382,16 @@ and try_coercions rdb
         (NCicPp.ppterm ~metasenv ~subst ~context expty))) exc)
   | (_,metasenv, newterm, newtype, meta)::tl ->
       try 
+          pp (lazy("K=" ^ NCicPp.ppterm ~metasenv ~subst ~context newterm));
           pp (lazy ( "UNIFICATION in CTX:\n"^ 
             NCicPp.ppcontext ~metasenv ~subst context
             ^ "\nMENV: " ^
             NCicPp.ppmetasenv metasenv ~subst
             ^ "\nOF: " ^
-            NCicPp.ppterm ~metasenv ~subst ~context meta ^  " === " ^
-            NCicPp.ppterm ~metasenv ~subst ~context t ^ "\n"));
+            NCicPp.ppterm ~metasenv ~subst ~context t ^  " === " ^
+            NCicPp.ppterm ~metasenv ~subst ~context meta ^ "\n"));
         let metasenv, subst = 
-          NCicUnification.unify rdb metasenv subst context meta t
+          NCicUnification.unify rdb metasenv subst context t meta
         in
           pp (lazy ( "UNIFICATION in CTX:\n"^ 
             NCicPp.ppcontext ~metasenv ~subst context
@@ -505,15 +508,13 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
       match NCicReduction.whd ~subst context ty_he with 
       | C.Prod (_,s,t) ->
           let metasenv, subst, arg, _ = 
-            typeof rdb ~localise 
-              metasenv subst context arg (Some s) in
+            typeof rdb ~localise metasenv subst context arg (Some s) in
           let t = NCicSubstitution.subst ~avoid_beta_redexes:true arg t in
           aux metasenv subst (arg :: args_so_far) he t tl
       | C.Meta _
       | C.Appl (C.Meta _ :: _) as t ->
           let metasenv, subst, arg, ty_arg = 
-            typeof rdb ~localise 
-              metasenv subst context arg None in
+            typeof rdb ~localise metasenv subst context arg None in
           let name = guess_name subst context ty_arg in
           let metasenv, _, meta, _ = 
             NCicMetaSubst.mk_meta metasenv 
@@ -522,8 +523,7 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
           let flex_prod = C.Prod (name, ty_arg, meta) in
           (* next line grants that ty_args is a type *)
           let metasenv,subst, flex_prod, _ =
-           typeof rdb ~localise metasenv subst
-            context flex_prod None in
+           typeof rdb ~localise metasenv subst context flex_prod None in
 (*
           pp (lazy ( "UNIFICATION in CTX:\n"^ 
             NCicPp.ppcontext ~metasenv ~subst context
@@ -810,6 +810,4 @@ let typeof_obj
       uri, height, metasenv, subst, C.Inductive (ind, leftno, itl, attr)
 ;;
 
-NCicUnification.set_refiner_typeof typeof;;
-
 (* vim:set foldmethod=marker: *)