allowed sort elim now check for recursive types

[helm.git] / helm / software / components / cic_unification / cicRefine.ml

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index fc9dc840d1bb5323ff9526ce57d561664b5999ac..956372d60294a621f2aa6941aea5a4cd51c02831 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1104,7 +1104,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
         | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) -> 
             let t' = CicUniv.fresh() in 
              (try
-              let ugraph1 = CicUniv.add_gt t' t1 ugraph in
+              let ugraph1 = CicUniv.add_ge t' t1 ugraph in
               let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
                 C.Sort (C.Type t'),subst,metasenv,ugraph2
               with
@@ -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 "")))