From 33dc2608260e6fdf02940a6845f4b0060017279c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 4 Nov 2005 17:18:12 +0000 Subject: [PATCH] refined outtype used to be discharged --- helm/ocaml/cic_unification/cicRefine.ml | 24 +++++++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index a0dfb9f28..9b9b02f7b 100644 --- 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 = -- 2.39.2