Better (but still broken) fix for the case ?sort vs ?term.

[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 a1ce81470d36d66dd4ae4fe99ef5c772fec95b4d..6664a5b9781cf0b06bb465c78f9f017558d6c522 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -380,15 +380,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 +506,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 +521,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 +808,4 @@ let typeof_obj
       uri, height, metasenv, subst, C.Inductive (ind, leftno, itl, attr)
 ;;
 
-NCicUnification.set_refiner_typeof typeof;;
-
 (* vim:set foldmethod=marker: *)