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.

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index e0f8fd1c79128ad1663640690a167c931ce623cb..f680b01f1e3cd2a75bc21c2b33729c8c3d8661ff 100644 (file)
--- a/components/cic_unification/cicRefine.ml
+++ b/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/components/cic_unification/coercGraph.ml b/components/cic_unification/coercGraph.ml
index 43e342e708f710ff27fcdb3f0aa41d00e6c4be5f..f12ea14b108e447951fe3691556d9ed760b88c8d 100644 (file)
--- a/components/cic_unification/coercGraph.ml
+++ b/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/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

diff --git a/components/cic_unification/termUtil.mli b/components/cic_unification/termUtil.mli
index 358b64616e7db4074a6f060fbfc00493037b6c88..c851bb5885576b403ac66087db3d11971cc915f2 100644 (file)
--- a/components/cic_unification/termUtil.mli
+++ b/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