X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FtermUtil.ml;h=1886b25d7dc05729ac35e7e75f3ac749c0cede09;hb=e68d06002f901a6252bc0b6ad6b655c9acb72b0f;hp=8905830be2757c9cf2816b11314cf2fc7edf5119;hpb=1d6910f6ee5dfd0e53fcec8c020311baba922a4c;p=helm.git

diff --git a/components/cic_unification/termUtil.ml b/components/cic_unification/termUtil.ml
index 8905830be..1886b25d7 100644
--- a/components/cic_unification/termUtil.ml
+++ b/components/cic_unification/termUtil.ml
@@ -31,7 +31,7 @@
 (* hypothesis, a list of arguments for the new applications and the index of  *)
 (* the last new META introduced. The nth argument in the list of arguments is *)
 (* just the nth new META.                                                     *)
-let saturate_term newmeta metasenv context ty goal_arity =
+let saturate_term ?(delta=true) newmeta metasenv context ty goal_arity =
  let module C = Cic in
  let module S = CicSubstitution in
  assert (goal_arity >= 0);
@@ -79,7 +79,7 @@ let saturate_term newmeta metasenv context ty goal_arity =
              lastmeta,prod_no + 1
     | t ->
        let head = CicReduction.normalize ~delta:false context t in
-        match CicReduction.whd context head with
+        match CicReduction.whd context head ~delta with
            C.Prod _ as head' -> aux newmeta head'
          | _ -> head,[],[],newmeta,0
   in