(* 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);
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