diff --git a/C/unify.c b/C/unify.c
index 0ab3c8e9f..86991f907 100644
--- a/C/unify.c
+++ b/C/unify.c
@@ -605,11 +605,13 @@ InitReverseLookupOpcode(void)
 }
 #endif
 
-#define UnifiableGlobalCells(a, b)                                    \
-     if((a) > (b)) {                                              \
-	Bind_Global_NonAtt((a),(CELL)(b));                           \
-     } else if((a) < (b)){                                        \
-	Bind_Global_NonAtt((b),(CELL) (a));                          \
+#define UnifyAndTrailGlobalCells(a, b)                                \
+     if((a) > (b)) {                                                  \
+       *(a) = (CELL)(b);                                              \
+        DO_TRAIL((a), (CELL)(b));                                     \
+     } else if((a) < (b)){                                            \
+       *(b) = (CELL)(a);                                              \
+        DO_TRAIL((b), (CELL)(a));                                     \
      }
 
 static int 
@@ -736,7 +738,8 @@ loop:
 
       derefa_body(d1, ptd1, unifiable_comp_nvar_unk, unifiable_comp_nvar_nvar);
 	/* d1 and pt2 have the unbound value, whereas d0 is bound */
-      Bind(ptd1, d0);
+      *(ptd1) = d0;
+      DO_TRAIL(ptd1, d0);
       continue;
     }
 
@@ -752,12 +755,13 @@ loop:
       deref_head(d1, unifiable_comp_var_unk);
     unifiable_comp_var_nvar:
       /* pt2 is unbound and d1 is bound */
-      Bind(ptd0, d1);
+      *ptd0 = d1;
+       DO_TRAIL(ptd0, d1);
       continue;
 
       derefa_body(d1, ptd1, unifiable_comp_var_unk, unifiable_comp_var_nvar);
       /* ptd0 and ptd1 are unbound */
-      UnifiableGlobalCells(ptd0, ptd1);
+      UnifyAndTrailGlobalCells(ptd0, ptd1);
     }
   }
   /* Do we still have compound terms to visit */
@@ -879,7 +883,8 @@ unifiable_nvar_nvar:
 
   deref_body(d1, pt1, unifiable_nvar_unk, unifiable_nvar_nvar);
   /* d0 is bound and d1 is unbound */
-  Bind(pt1, d0);
+  *(pt1) = d0;
+  DO_TRAIL(pt1, d0);
   return (TRUE);
 
   deref_body(d0, pt0, unifiable_unk, unifiable_nvar);
@@ -887,18 +892,13 @@ unifiable_nvar_nvar:
   deref_head(d1, unifiable_var_unk);
 unifiable_var_nvar:
   /* pt0 is unbound and d1 is bound */
-  Bind(pt0, d1);
+  *pt0 = d1;
+   DO_TRAIL(pt0, d1);
   return TRUE;
 
-#if TRAILING_REQUIRES_BRANCH
-unifiable_var_nvar_trail:
-  DO_TRAIL(pt0);
-  return TRUE;
-#endif
-
   deref_body(d1, pt1, unifiable_var_unk, unifiable_var_nvar);
   /* d0 and pt1 are unbound */
-  UnifyCells(pt0, pt1);
+  UnifyAndTrailCells(pt0, pt1);
   return (TRUE);
 #if THREADS
 #undef Yap_REGS
@@ -914,13 +914,13 @@ unifiable_var_nvar_trail:
 static Int
 p_unifiable( USES_REGS1 )
 {
-  tr_fr_ptr trp;
+  tr_fr_ptr trp, trp0 = TR;
   Term tf = TermNil;
   if (!unifiable(ARG1,ARG2)) {
     return FALSE;
   }
   trp = TR;
-  while (trp != B->cp_tr) {
+  while (trp != trp0) {
     Term t[2];
     --trp;
     t[0] = TrailTerm(trp);
@@ -931,6 +931,26 @@ p_unifiable( USES_REGS1 )
   return Yap_unify(ARG3, tf);
 }
 
+int
+Yap_unifiable( Term d0, Term d1 )
+{
+  CACHE_REGS
+  tr_fr_ptr trp, trp0 = TR;
+  Term tf = TermNil;
+  if (!unifiable(d0,d1)) {
+    return FALSE;
+  }
+  trp = TR;
+  while (trp != trp0) {
+    Term t;
+
+    --trp;
+    t = TrailTerm(trp);
+    RESET_VARIABLE(t);
+  }
+  return TRUE;
+}
+
 void 
 Yap_InitUnify(void)
 {
@@ -940,7 +960,7 @@ Yap_InitUnify(void)
   Yap_InitCPred("acyclic_term", 1, p_acyclic, SafePredFlag|TestPredFlag);
   CurrentModule = TERMS_MODULE;
   Yap_InitCPred("cyclic_term", 1, p_cyclic, SafePredFlag|TestPredFlag);
-  Yap_InitCPred("protected_unifiable", 3, p_unifiable, 0);
+  Yap_InitCPred("unifiable", 3, p_unifiable, 0);
   CurrentModule = cm;
 }
 
diff --git a/H/absmi.h b/H/absmi.h
index ba5926a6c..a5e6eda21 100644
--- a/H/absmi.h
+++ b/H/absmi.h
@@ -1583,3 +1583,16 @@ void SET_ASP__(CELL *yreg, Int sz USES_REGS) {
 #define INITIALIZE_PERMVAR(PTR, V) *(PTR) = (V)
 #endif
 
+/* l1: bind a, l2 bind b, l3 no binding */
+#define UnifyAndTrailCells(a, b)                                            \
+     if((a) > (b)) {                                                        \
+       if ((a) < H) { *(a) = (CELL)(b); DO_TRAIL((a),(CELL)(b)); }	    \
+       else if ((b) <= H) { *(a) =(CELL)(b); DO_TRAIL((a),(CELL)(b));}	   \
+       else { *(b) = (CELL)(a);  DO_TRAIL((b),(CELL)(a)); }		    \
+     } else if((a) < (b)){                                                  \
+       if ((b) <= H) { *(b) = (CELL)(a); DO_TRAIL((b),(CELL)(a)); }         \
+       else if ((a) <= H) { *(b) = (CELL) (a); DO_TRAIL((b),(CELL)(a));}    \
+       else { *(a) = (CELL) (b);  DO_TRAIL((a),(CELL)(b));}                 \
+     }
+
+
diff --git a/docs/yap.tex b/docs/yap.tex
index c93c4dd27..dd4d5d2f9 100644
--- a/docs/yap.tex
+++ b/docs/yap.tex
@@ -16182,6 +16182,27 @@ of non-variable terms:
       YAP_Bool YAP_IsApplTerm(YAP_Term @var{t})
 @end example
 
+The next primitive gives the type of a Prolog term:
+@example
+      YAP_tag_t YAP_TagOfTerm(YAP_Term @var{t})
+@end example
+The set of possible values is an enumerated type, with the following values:
+@table @i
+@item  @code{YAP_TAG_ATT}: an attributed variable
+@item  @code{YAP_TAG_UNBOUND}: an unbound variable
+@item  @code{YAP_TAG_REF}: a reference to a term
+@item  @code{YAP_TAG_PAIR}: a list
+@item  @code{YAP_TAG_ATOM}: an atom
+@item  @code{YAP_TAG_INT}: a small integer
+@item  @code{YAP_TAG_LONG_INT}: a word sized integer
+@item  @code{YAP_TAG_BIG_INT}: a very large integer
+@item  @code{YAP_TAG_RATIONAL}: a rational number
+@item  @code{YAP_TAG_FLOAT}: a floating point number
+@item  @code{YAP_TAG_OPAQUE}: an opaque term
+@item  @code{YAP_TAG_APPL}: a compound term
+@end table
+
+
 Next, we mention the primitives that allow one to destruct and construct
 terms. All the above primitives ensure that their result is
 @i{dereferenced}, i.e. that it is not a pointer to another term.
@@ -16567,14 +16588,14 @@ lead to a crash.
 The following functions are often required to compare terms.
 
 @findex YAP_ExactlyEqual (C-Interface function)
-The first function succeeds if two terms are actually the same term, as
+Succeed if two terms are actually the same term, as in
 @code{==/2}:
 @example
       int      YAP_ExactlyEqual(YAP_Term t1, YAP_Term t2)
 @end example
 @noindent
 
-The second function succeeds if two terms are variant terms, and returns
+The next function succeeds if two terms are variant terms, and returns
 0 otherwise, as
 @code{=@=/2}:
 @example
@@ -16582,6 +16603,13 @@ The second function succeeds if two terms are variant terms, and returns
 @end example
 @noindent
 
+Last, this function succeeds if two terms are unifiable:
+@code{=@=/2}:
+@example
+      int      YAP_Unifiable(YAP_Term t1, YAP_Term t2)
+@end example
+@noindent
+
 The second function computes a hash function for a term, as in
 @code{term_hash/4}.
 @example
diff --git a/include/YapInterface.h b/include/YapInterface.h
index 5cd333869..cc6986bdb 100644
--- a/include/YapInterface.h
+++ b/include/YapInterface.h
@@ -534,6 +534,7 @@ extern X_API int        PROTO(YAP_Erase,(void *));
 
 /*  term utilities */
 extern X_API int        PROTO(YAP_Variant,(YAP_Term,YAP_Term));
+extern X_API int        PROTO(YAP_Unifiable,(YAP_Term,YAP_Term));
 extern X_API int        PROTO(YAP_ExactlyEqual,(YAP_Term,YAP_Term));
 extern X_API YAP_Int    PROTO(YAP_TermHash,(YAP_Term, YAP_Int, YAP_Int, int));
 
@@ -570,6 +571,8 @@ extern X_API void *PROTO(YAP_OpaqueObjectFromTerm,(YAP_Term));
 
 extern X_API int *PROTO(YAP_Argv,(char ***));
 
+extern X_API YAP_tag_t PROTO(YAP_TagOfTerm,(YAP_Term));
+
 #define YAP_InitCPred(N,A,F)  YAP_UserCPredicate(N,F,A)
 
 __END_DECLS