X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FtermUtil.ml;h=1886b25d7dc05729ac35e7e75f3ac749c0cede09;hb=b637879a2b3f2ceda65afb3c950061189c4730b7;hp=8905830be2757c9cf2816b11314cf2fc7edf5119;hpb=5d010a40c726d9a7eceeb35e70e41a158eb63c70;p=helm.git

diff --git a/helm/software/components/cic_unification/termUtil.ml b/helm/software/components/cic_unification/termUtil.ml
index 8905830be..1886b25d7 100644
--- a/helm/software/components/cic_unification/termUtil.ml
+++ b/helm/software/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