From 25f486e24d9d34e85476414771b4d01d2c468299 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Jun 2005 13:47:53 +0000 Subject: [PATCH] Fixed a few bugs in the inference of the outtype for a match. In particular the instances of the left parameter that occur in the outtype were not lifted properly because of the abstractions that correspond to the right parameters. --- helm/ocaml/cic_unification/cicRefine.ml | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 351104f56..8828a417e 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -460,9 +460,13 @@ and type_of_aux' metasenv context t ugraph = function 0 -> [] | n -> (Cic.Rel n)::(mk_right_args (n - 1)) + in + let right_args_no = List.length right_args in + let lifted_left_args = + List.map (CicSubstitution.lift right_args_no) left_args in Cic.Appl (Cic.MutInd(uri,i,exp_name_subst):: - (left_args @ mk_right_args (List.length right_args))) + (lifted_left_args @ mk_right_args right_args_no)) in let fresh_name = FreshNamesGenerator.mk_fresh_name ~subst metasenv @@ -471,13 +475,16 @@ and type_of_aux' metasenv context t ugraph = match outtypeinstances with | [] -> let extended_context = - let rec add_right_args b = + let rec add_right_args = function Cic.Prod (name,ty,t) -> - Some (name,Cic.Decl ty)::(add_right_args b t) - | _ -> (Some (fresh_name,Cic.Decl ty))::b + Some (name,Cic.Decl ty)::(add_right_args t) + | _ -> [] in - add_right_args context arity_instantiated_with_left_args + (Some (fresh_name,Cic.Decl ty)):: + (List.rev + (add_right_args arity_instantiated_with_left_args))@ + context in let metasenv,new_meta = CicMkImplicit.mk_implicit metasenv subst extended_context -- 2.39.2