Refinement of inductive type implemented.

[helm.git] / helm / software / components / ng_refiner / nCicUnification.ml

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 3000b7311dca621bcedfc3464380621c13d3e2a6..f178fc4b780f824143bd19af4cb2dca2b85b52fb 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -612,8 +612,6 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
  (*D*)  in outside(); rc with exn -> outside (); raise exn 
 ;;
 
-let unify hdb = 
+let unify hdb ?(test_eq_only=false) = 
   indent := "";      
-  unify hdb false;;
-
-
+  unify hdb test_eq_only;;