From 70211a10f741fe77945f5a720596df2b686f344d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 10 Jul 2008 08:00:30 +0000
Subject: [PATCH 1/1] fixed regression in casting an argument to funclass, this
 incidentally leaded to a single look_for_coercion_function

---
 .../components/cic_unification/cicRefine.ml      |  8 +++++---
 .../components/cic_unification/coercGraph.ml     | 16 ++++++++++++----
 .../components/cic_unification/coercGraph.mli    |  4 ----
 3 files changed, 17 insertions(+), 11 deletions(-)

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index fc9dc840d..bde5d63e4 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1251,9 +1251,11 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
     (* given he:hety, gives beack all (c he) such that (c e):?->? *)
     let fix_arity n metasenv context subst he hetype ugraph =
       let hetype = CicMetaSubst.apply_subst subst hetype in
-      let src = CoercDb.coerc_carr_of_term hetype 0 in 
-      let tgt = CoercDb.coerc_carr_of_term (Cic.Implicit None) 1 in
-      match CoercGraph.look_for_coercion' metasenv subst context src tgt with
+      (* instead of a dummy functional type we may create the real product
+       * using args_bo_and_ty, but since coercions lookup ignores the 
+       * actual ariety we opt for the simple solution *)
+      let fty = Cic.Prod(Cic.Anonymous, Cic.Sort Cic.Prop, Cic.Sort Cic.Prop) in
+      match CoercGraph.look_for_coercion metasenv subst context hetype fty with
       | CoercGraph.NoCoercion -> []
       | CoercGraph.NotHandled ->
          raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
diff --git a/helm/software/components/cic_unification/coercGraph.ml b/helm/software/components/cic_unification/coercGraph.ml
index 637944e6b..2fa2c4b0c 100644
--- a/helm/software/components/cic_unification/coercGraph.ml
+++ b/helm/software/components/cic_unification/coercGraph.ml
@@ -70,7 +70,7 @@ let saturate_coercion ul metasenv subst context =
 ;;
           
 (* searches a coercion fron src to tgt in the !coercions list *)
-let look_for_coercion' metasenv subst context src tgt =
+let look_for_coercion_carr metasenv subst context src tgt =
   let is_dead = function CoercDb.Dead -> true | _ -> false in
   let pp_l s l =
    match l with
@@ -108,10 +108,18 @@ let look_for_coercion' metasenv subst context src tgt =
      | ul -> SomeCoercion (saturate_coercion ul metasenv subst context))
 ;;
 
+let rec count_pi c s t =
+  match CicReduction.whd ~delta:false ~subst:s c t with
+  | Cic.Prod (_,_,t) -> 1 + count_pi c s t
+  | _ -> 0
+;;
+
 let look_for_coercion metasenv subst context src tgt = 
-  let src_uri = CoercDb.coerc_carr_of_term src 0 in
-  let tgt_uri = CoercDb.coerc_carr_of_term tgt 0 in
-  look_for_coercion' metasenv subst context src_uri tgt_uri
+  let src_arity = count_pi context subst src in
+  let tgt_arity = count_pi context subst tgt in
+  let src_carr = CoercDb.coerc_carr_of_term src src_arity in
+  let tgt_carr = CoercDb.coerc_carr_of_term tgt tgt_arity in
+  look_for_coercion_carr metasenv subst context src_carr tgt_carr
 
 let source_of t = 
   match CoercDb.is_a_coercion t with
diff --git a/helm/software/components/cic_unification/coercGraph.mli b/helm/software/components/cic_unification/coercGraph.mli
index 1a3be89f3..abc94688c 100644
--- a/helm/software/components/cic_unification/coercGraph.mli
+++ b/helm/software/components/cic_unification/coercGraph.mli
@@ -40,10 +40,6 @@ val look_for_coercion :
   Cic.metasenv -> Cic.substitution -> Cic.context ->
    Cic.term -> Cic.term -> coercion_search_result
 
-val look_for_coercion' :
-  Cic.metasenv -> Cic.substitution -> Cic.context ->
-   CoercDb.coerc_carr -> CoercDb.coerc_carr -> coercion_search_result
-
 (* checks if term is a constant or 
  * a constant applyed that is marked with (`Class `Coercion) *)
 val is_composite: Cic.term -> bool
-- 
2.39.2