added ~delta parameter to saturate_term and used it when saturating a coercion.

[helm.git] / components / cic_unification / termUtil.ml

diff --git a/components/cic_unification/termUtil.ml b/components/cic_unification/termUtil.ml
index 8905830be2757c9cf2816b11314cf2fc7edf5119..1886b25d7dc05729ac35e7e75f3ac749c0cede09 100644 (file)
--- 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