thanks to the fact that we convert well typed term and that

we convert only types, by inversion we know that types of lambdas
source are convertible if in head position

diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml
index 0d19524dcf1842d2667f36de5286b7adfdfb8ba0..c16b11159c38ccde56621da9d3b9c97c611419c9 100644 (file)
--- a/helm/software/components/extlib/hExtlib.ml
+++ b/helm/software/components/extlib/hExtlib.ml
@@ -515,3 +515,8 @@ let chop_prefix prefix s =
 let touch s =
   try close_out(open_out s) with Sys_error _ -> ()
 ;;
+
+let rec mk_list x = function
+  | 0 -> []
+  | n -> x :: mk_list x (n-1)
+;;

diff --git a/helm/software/components/extlib/hExtlib.mli b/helm/software/components/extlib/hExtlib.mli
index 1e2d8e04710ab55be1303d6c59b825bdceced20b..594a80027956644cb721f3007a97c34a678adfa1 100644 (file)
--- a/helm/software/components/extlib/hExtlib.mli
+++ b/helm/software/components/extlib/hExtlib.mli
@@ -108,6 +108,7 @@ val list_forall_default3: ('a -> 'b -> 'c -> bool) -> 'a list -> 'b list -> 'c -
    * @raise Failure when List.length l < n *)
 val split_nth: int -> 'a list -> 'a list * 'a list
 
+val mk_list: 'a -> int -> 'a list
 (** {2 Debugging & Profiling} *)
 
 type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b }

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index c6abbd0e03968529ef960cac19c5cdbe11322181..4ff6af692bdb924fa651b937cdebe6b942131c99 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -188,8 +188,9 @@ let are_convertible ?(subst=[])  =
        | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
            aux true context s1 s2 &&
            aux test_eq_only ((name1, C.Decl s1)::context) t1 t2
-       | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
-          aux true context s1 s2 && 
+       | (C.Lambda (name1,s1,t1), C.Lambda(_,_,t2)) ->
+          (* thanks to inversion of well typedness, the source 
+           * of these lambdas must be already convertible *)
           aux test_eq_only ((name1, C.Decl s1)::context) t1 t2
        | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
           aux test_eq_only context ty1 ty2 &&
@@ -224,6 +225,13 @@ let are_convertible ?(subst=[])  =
        | (C.Appl (C.Const r1::tl1), C.Appl (C.Const r2::tl2)) ->
           r1 = r2 &&
            let relevance = NCicEnvironment.get_relevance r1 in
+           let relevance = 
+             match r1 with 
+             | Ref.Ref (_,Ref.Con (_,_,lno)) -> 
+                 let _,relevance = HExtlib.split_nth lno relevance in
+                 HExtlib.mk_list false lno @ relevance
+             | _ -> relevance 
+           in
            (try
              HExtlib.list_forall_default3
               (fun t1 t2 b -> not b || aux test_eq_only context t1 t2)