From edc5e28c59721e358e5d0bc32a7a44d500918386 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 15 Nov 2007 09:20:34 +0000
Subject: [PATCH] added ~delta parameter to saturate_term and used it when
 saturating a coercion. it is always true that the user wants the type of its
 coercion no to be unfolded, since its arity was computed without unfolding.

---
 helm/software/components/cic_unification/cicRefine.ml  | 4 +++-
 helm/software/components/cic_unification/coercGraph.ml | 2 +-
 helm/software/components/cic_unification/termUtil.ml   | 4 ++--
 helm/software/components/cic_unification/termUtil.mli  | 1 +
 4 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index e0f8fd1c7..f680b01f1 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1334,7 +1334,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                 (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
                 CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
                 " <==> " ^
-                CicMetaSubst.ppterm_in_context ~metasenv subst t context));
+                CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ 
+                "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c
+                context));
                 debug_print (lazy ("FO_UNIF_SUBST: " ^
                 CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
                 let subst,metasenv,ugraph =
diff --git a/helm/software/components/cic_unification/coercGraph.ml b/helm/software/components/cic_unification/coercGraph.ml
index 43e342e70..f12ea14b1 100644
--- a/helm/software/components/cic_unification/coercGraph.ml
+++ b/helm/software/components/cic_unification/coercGraph.ml
@@ -54,7 +54,7 @@ let saturate_coercion ul metasenv subst context =
        CicTypeChecker.type_of_aux' ~subst metasenv context c
         CicUniv.empty_ugraph in
       let _,metasenv,args,lastmeta =
-       TermUtil.saturate_term freshmeta metasenv context ty arity in
+       TermUtil.saturate_term ~delta:false freshmeta metasenv context ty arity in
       let irl =
        CicMkImplicit.identity_relocation_list_for_metavariable context
       in
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
diff --git a/helm/software/components/cic_unification/termUtil.mli b/helm/software/components/cic_unification/termUtil.mli
index 358b64616..c851bb588 100644
--- a/helm/software/components/cic_unification/termUtil.mli
+++ b/helm/software/components/cic_unification/termUtil.mli
@@ -32,5 +32,6 @@
 (* the last new META introduced. The nth argument in the list of arguments is *)
 (* just the nth new META.                                                     *)
 val saturate_term:
+ ?delta: bool -> (* default true *)
  int -> Cic.metasenv -> Cic.context -> Cic.term -> int ->
   Cic.term * Cic.metasenv * Cic.term list * int
-- 
2.39.2