From: Claudio Sacerdoti Coen Date: Fri, 8 May 2009 22:07:55 +0000 (+0000) Subject: Bug fixed: left parameters of constructors were unified before refining them. X-Git-Tag: make_still_working~4003 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6f676b9124d4630e986f490fda0ae584a3a287ba;p=helm.git Bug fixed: left parameters of constructors were unified before refining them. Fixed, but the new code typechecks the constructors twice (in order to re-compute) the sort without the inductive types. Is a more efficient implementation worth the effort? --- diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 7cc2f33d2..4198eae5f 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -538,6 +538,7 @@ let typeof_obj hdb ?(localise=fun _ -> Stdpp.dummy_loc) ~look_for_coercion (uri,height,metasenv,subst,obj) = +prerr_endline ("===============\n" ^ NCicPp.ppobj (uri,height,metasenv,subst,obj)); let check_type metasenv subst context (ty as orig_ty) = (* XXX fattorizza *) let metasenv, subst, ty, sort = typeof hdb ~localise ~look_for_coercion metasenv subst context ty None @@ -621,6 +622,7 @@ let typeof_obj hdb try snd (HExtlib.split_nth leftno k_relev) with Failure _ -> k_relev in let te = NCicTypeChecker.debruijn uri len [] te in + let metasenv, subst, te, _ = check_type metasenv subst tys te in let context,te = NCicReduction.split_prods ~subst tys leftno te in let _,chopped_context_rev = HExtlib.split_nth (List.length tys) (List.rev context) in @@ -666,11 +668,8 @@ let typeof_obj hdb else metasenv,subst,item1::context ) (metasenv,subst,[]) sx_context_ty_rev sx_context_te_rev - with Invalid_argument "List.fold_left2" -> assert false - in - let metasenv, subst, te, con_sort = - check_type metasenv subst context te - in + with Invalid_argument "List.fold_left2" -> assert false in + let con_sort= NCicTypeChecker.typeof ~subst ~metasenv context te in (match NCicReduction.whd ~subst context con_sort, NCicReduction.whd ~subst [] ty_sort