refined outtype used to be discharged

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index a0dfb9f2889e2d7bb024a1e08b28c8d756616078..9b9b02f7bf633ed160ea9eef4a99542f5529d7bd 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -480,7 +480,7 @@ and type_of_aux' metasenv context t ugraph =
                 ) tl ([],subst',metasenv',ugraph1)
             in
             let tl',applty,subst''',metasenv''',ugraph3 =
-              eat_prods subst'' metasenv'' context 
+              eat_prods true subst'' metasenv'' context 
                 hetype tlbody_and_type ugraph2
             in
               C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
@@ -743,6 +743,22 @@ and type_of_aux' metasenv context t ugraph =
                         (Cic.Appl (outtype::right_args@[term']))),
                      subst,metasenv,ugraph)
            | _ ->    (* easy case *)
+             let outtype,outtypety, subst, metasenv,ugraph4 =
+               type_of_aux subst metasenv context outtype ugraph4
+             in
+             let tlbody_and_type,subst,metasenv,ugraph4 =
+               List.fold_right
+                 (fun x (res,subst,metasenv,ugraph) ->
+                    let x',ty,subst',metasenv',ugraph1 =
+                      type_of_aux subst metasenv context x ugraph
+                    in
+                      (x', ty)::res,subst',metasenv',ugraph1
+                 ) (right_args @ [term']) ([],subst,metasenv,ugraph4)
+             in
+             let _,_,subst,metasenv,ugraph4 =
+               eat_prods false subst metasenv context 
+                 outtypety tlbody_and_type ugraph4
+             in
              let _,_, subst, metasenv,ugraph5 =
                type_of_aux subst metasenv context
                  (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
@@ -1000,7 +1016,9 @@ and type_of_aux' metasenv context t ugraph =
                 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
                 (CicPp.ppterm t2''))))
 
-  and eat_prods subst metasenv context hetype tlbody_and_type ugraph =
+  and eat_prods 
+    allow_coercions subst metasenv context hetype tlbody_and_type ugraph 
+  =
     let rec mk_prod metasenv context =
       function
           [] ->
@@ -1067,7 +1085,7 @@ and type_of_aux' metasenv context t ugraph =
                          fo_unif_subst subst context metasenv hety s ugraph
                        in
                          hete,subst,metasenv,ugraph1
-                     with exn ->
+                     with exn when allow_coercions ->
                        (* we search a coercion from hety to s *)
                        let coer = 
                          let carr t subst context =