From da178a880e3ace820b41d38b191d3785b82991f5 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 1 Jul 2010 17:21:14 +0200 Subject: Imported Upstream version 8.2pl2+dfsg --- pretyping/cases.ml | 12 +++++--- pretyping/clenv.ml | 13 ++++---- pretyping/clenv.mli | 4 ++- pretyping/detyping.ml | 5 ++-- pretyping/evarconv.ml | 30 ++++++++++++------- pretyping/evarutil.ml | 77 ++++++++++++++++++++++++++++++++++++++++-------- pretyping/evarutil.mli | 4 +-- pretyping/tacred.ml | 52 +++++++++++++++++++++----------- pretyping/unification.ml | 4 +-- 9 files changed, 144 insertions(+), 57 deletions(-) (limited to 'pretyping') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index c2d8921e..abe4fcc1 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cases.ml 12167 2009-06-06 20:07:22Z herbelin $ *) +(* $Id: cases.ml 13112 2010-06-10 19:58:23Z herbelin $ *) open Util open Names @@ -851,7 +851,7 @@ let rec map_predicate f k ccl = function | Abstract _ :: rest -> map_predicate f (k+1) ccl rest -let noccurn_predicate = map_predicate noccurn +let noccur_predicate_between n = map_predicate (noccur_between n) let liftn_predicate n = map_predicate (liftn n) @@ -1122,13 +1122,16 @@ let build_branch current deps (realnames,dep) pb eqns const_info = (* into "Gamma; typs; curalias |- tms" *) let tomatch = lift_tomatch_stack const_info.cs_nargs pb.tomatch in + let pred_is_not_dep = + noccur_predicate_between 1 (List.length realnames + 1) pb.pred tomatch in + let typs'' = list_map2_i (fun i (na,t) deps -> let dep = match dep with | Name _ as na',k -> (if na <> Anonymous then na else na'),k | Anonymous,KnownNotDep -> - if deps = [] && noccurn_predicate 1 pb.pred tomatch then + if deps = [] && pred_is_not_dep then (Anonymous,KnownNotDep) else (force_name na,KnownDep) @@ -1801,7 +1804,8 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon pred = let t2 = mkExistential env ~src:(loc, CasesType) evdref2 in let arsign = extract_arity_signature env tomatchs sign in let names2 = List.rev (List.map (List.map pi1) arsign) in - let nal2,pred2 = build_initial_predicate KnownNotDep names2 t2 in + let pred2 = lift (List.length names2) t2 in + let nal2,pred2 = build_initial_predicate KnownNotDep names2 pred2 in [evdref, nal1, pred1; evdref2, nal2, pred2]) (* Some type annotation *) diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 51952f4f..0bfef04a 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: clenv.ml 11897 2009-02-09 19:28:02Z barras $ *) +(* $Id: clenv.ml 13126 2010-06-13 11:09:51Z herbelin $ *) open Pp open Util @@ -410,8 +410,9 @@ let clenv_unify_binding_type clenv c t u = try let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in TypeProcessed, { clenv with evd = evd }, c - with e when precatchable_exception e -> - TypeNotProcessed, clenv, c + with + | PretypeError (_,NotClean _) as e -> raise e + | e when precatchable_exception e -> TypeNotProcessed, clenv, c let clenv_assign_binding clenv k (sigma,c) = let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in @@ -436,11 +437,11 @@ let clenv_match_args bl clenv = clenv_assign_binding clenv k sc) clenv bl +exception NoSuchBinding + let clenv_constrain_last_binding c clenv = let all_mvs = collect_metas clenv.templval.rebus in - let k = - try list_last all_mvs - with Failure _ -> anomaly "clenv_constrain_with_bindings" in + let k = try list_last all_mvs with Failure _ -> raise NoSuchBinding in clenv_assign_binding clenv k (Evd.empty,c) let clenv_constrain_dep_args hyps_only bl clenv = diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index 9b2d6e29..4c5535b3 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: clenv.mli 10856 2008-04-27 16:15:34Z herbelin $ i*) +(*i $Id: clenv.mli 13126 2010-06-13 11:09:51Z herbelin $ i*) (*i*) open Util @@ -94,6 +94,8 @@ type arg_bindings = open_constr explicit_bindings val clenv_independent : clausenv -> metavariable list val clenv_missing : clausenv -> metavariable list +(** for the purpose of inversion tactics *) +exception NoSuchBinding val clenv_constrain_last_binding : constr -> clausenv -> clausenv (* defines metas corresponding to the name of the bindings *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 73dc5d46..20cbba94 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: detyping.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: detyping.ml 12887 2010-03-27 15:57:02Z herbelin $ *) open Pp open Util @@ -329,7 +329,6 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = n, aliastyp, Some typ in let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in - let eqnl = detype_eqns constructs consnargsl bl in let tag = try if !Flags.raw_print then @@ -357,8 +356,10 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = RIf (dl,tomatch,(alias,pred), Option.get nondepbrs.(0),Option.get nondepbrs.(1)) else + let eqnl = detype_eqns constructs consnargsl bl in RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl) | _ -> + let eqnl = detype_eqns constructs consnargsl bl in RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl) let detype_sort = function diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 043a326d..18e79e85 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarconv.ml 12205 2009-06-22 16:10:15Z barras $ *) +(* $Id: evarconv.ml 12268 2009-08-11 09:02:16Z herbelin $ *) open Pp open Util @@ -66,6 +66,10 @@ let apprec_nohdbeta env evd c = | (Case _ | Fix _) -> applist (evar_apprec env evd [] c) | _ -> c +let position_problem l2r = function + | CONV -> None + | CUMUL -> Some l2r + (* [check_conv_record (t1,l1) (t2,l2)] tries to decompose the problem (t1 l1) = (t2 l2) into a problem @@ -177,9 +181,11 @@ let rec evar_conv_x env evd pbty term1 term2 = let term1 = apprec_nohdbeta env evd term1 in let term2 = apprec_nohdbeta env evd term2 in if is_undefined_evar evd term1 then - solve_simple_eqn evar_conv_x env evd (pbty,destEvar term1,term2) + solve_simple_eqn evar_conv_x env evd + (position_problem true pbty,destEvar term1,term2) else if is_undefined_evar evd term2 then - solve_simple_eqn evar_conv_x env evd (pbty,destEvar term2,term1) + solve_simple_eqn evar_conv_x env evd + (position_problem false pbty,destEvar term2,term1) else evar_eqappr_x env evd pbty (decompose_app term1) (decompose_app term2) @@ -193,14 +199,14 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in ise_and i [(fun i -> solve_simple_eqn evar_conv_x env i - (pbty,ev2,applist(term1,deb1))); + (position_problem false pbty,ev2,applist(term1,deb1))); (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest1 l2)] else let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in ise_and i [(fun i -> solve_simple_eqn evar_conv_x env i - (pbty,ev1,applist(term2,deb2))); + (position_problem true pbty,ev1,applist(term2,deb2))); (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) l1 rest2)] and f2 i = @@ -224,7 +230,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = (* Preserve generality (except that CCI has no eta-conversion) *) let t2 = nf_evar (evars_of evd) (applist appr2) in let t2 = solve_pattern_eqn env l1 t2 in - solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2) + solve_simple_eqn evar_conv_x env evd + (position_problem true pbty,ev1,t2) else if List.length l1 <= List.length l2 then @@ -256,7 +263,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = (* Preserve generality (except that CCI has no eta-conversion) *) let t1 = nf_evar (evars_of evd) (applist appr1) in let t1 = solve_pattern_eqn env l2 t1 in - solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1) + solve_simple_eqn evar_conv_x env evd + (position_problem false pbty,ev2,t1) else if List.length l2 <= List.length l1 then @@ -324,7 +332,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = (* Preserve generality (except that CCI has no eta-conversion) *) let t2 = nf_evar (evars_of evd) (applist appr2) in let t2 = solve_pattern_eqn env l1 t2 in - solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2) + solve_simple_eqn evar_conv_x env evd + (position_problem true pbty,ev1,t2) else (* Postpone the use of an heuristic *) add_conv_pb (pbty,env,applist appr1,applist appr2) evd, @@ -339,7 +348,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = (* Preserve generality (except that CCI has no eta-conversion) *) let t1 = nf_evar (evars_of evd) (applist appr1) in let t1 = solve_pattern_eqn env l2 t1 in - solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1) + solve_simple_eqn evar_conv_x env evd + (position_problem false pbty,ev2,t1) else (* Postpone the use of an heuristic *) add_conv_pb (pbty,env,applist appr1,applist appr2) evd, @@ -505,7 +515,7 @@ let first_order_unification env evd (ev1,l1) (term2,l2) = if is_defined_evar i ev1 then evar_conv_x env i CONV t2 (mkEvar ev1) else - solve_simple_eqn ~choose:true evar_conv_x env i (CONV,ev1,t2))] + solve_simple_eqn ~choose:true evar_conv_x env i (None,ev1,t2))] let choose_less_dependent_instance evk evd term args = let evi = Evd.find (evars_of evd) evk in diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 994da427..fbaac79b 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarutil.ml 12107 2009-04-25 19:58:24Z herbelin $ *) +(* $Id: evarutil.ml 13116 2010-06-12 15:18:07Z herbelin $ *) open Util open Pp @@ -113,11 +113,27 @@ let push_dependent_evars sigma emap = (sigma',emap') (collect_evars emap' ccl)) emap (sigma,emap) +let push_duplicated_evars sigma emap c = + let rec collrec (one,(sigma,emap) as acc) c = + match kind_of_term c with + | Evar (evk,_) when not (Evd.mem sigma evk) -> + if List.mem evk one then + let sigma' = Evd.add sigma evk (Evd.find emap evk) in + let emap' = Evd.remove emap evk in + (one,(sigma',emap')) + else + (evk::one,(sigma,emap)) + | _ -> + fold_constr collrec acc c + in + snd (collrec ([],(sigma,emap)) c) + (* replaces a mapping of existentials into a mapping of metas. Problem if an evar appears in the type of another one (pops anomaly) *) let evars_to_metas sigma (emap, c) = let emap = nf_evars emap in let sigma',emap' = push_dependent_evars sigma emap in + let sigma',emap' = push_duplicated_evars sigma' emap' c in let change_exist evar = let ty = nf_betaiota emap (existential_type emap evar) in let n = new_meta() in @@ -559,6 +575,7 @@ let rec expansions_of_var env x = *) exception NotUnique +exception NotUniqueInType of types type evar_projection = | ProjectVar @@ -570,12 +587,13 @@ let rec find_projectable_vars with_evars env sigma y subst = if y = y' or expand_var env y = expand_var env y' then (idc,(y'=y,(id,ProjectVar))) else if with_evars & isEvar y' then + (* TODO: infer conditions for being of unifiable types *) let (evk,argsv as t) = destEvar y' in let evi = Evd.find sigma evk in let subst = make_projectable_subst sigma evi argsv in let l = find_projectable_vars with_evars env sigma y subst in match l with - | [id',p] -> (idc,(true,(id,ProjectEvar (t,evi,id',p)))) + | [id',p] -> (idc,(true,(id,ProjectEvar(t,evi,id',p)))) | _ -> failwith "" else failwith "" in let l = map_succeed is_projectable subst in @@ -596,6 +614,12 @@ let project_with_effects env sigma effects t subst = effects := p :: !effects; c +let rec find_solution_type evarenv = function + | (id,ProjectVar)::l -> pi3 (lookup_named id evarenv) + | [id,ProjectEvar _] -> (* bugged *) pi3 (lookup_named id evarenv) + | (id,ProjectEvar _)::l -> find_solution_type evarenv l + | [] -> assert false + (* In case the solution to a projection problem requires the instantiation of * subsidiary evars, [do_projection_effects] performs them; it * also try to instantiate the type of those subsidiary evars if their @@ -709,7 +733,7 @@ let filter_along f projs v = * such that "hyps' |- ?e : T" *) -let do_restrict_hyps_virtual evd evk filter = +let restrict_hyps evd evk filter = (* What to do with dependencies? Assume we have x:A, y:B(x), z:C(x,y) |- ?e:T(x,y,z) and restrict on y. - If y is in a non-erasable position in C(x,y) (i.e. it is not below an @@ -726,15 +750,15 @@ let do_restrict_hyps_virtual evd evk filter = let filter,_ = List.fold_right (fun oldb (l,filter) -> if oldb then List.hd filter::l,List.tl filter else (false::l,filter)) oldfilter ([],List.rev filter) in - new_evar evd env ~src:(evar_source evk evd) - ~filter:filter evi.evar_concl + (env,evar_source evk evd,filter,evi.evar_concl) let do_restrict_hyps evd evk projs = let filter = List.map filter_of_projection projs in if List.for_all (fun x -> x) filter then evd,evk else - let evd,nc = do_restrict_hyps_virtual evd evk filter in + let env,src,filter,ccl = restrict_hyps evd evk filter in + let evd,nc = new_evar evd env ~src ~filter ccl in let evd = Evd.evar_define evk nc evd in let evk',_ = destEvar nc in evd,evk' @@ -854,7 +878,9 @@ let rec invert_definition choose env evd (evk,argsv as ev) rhs = let c, p = match sols with | [] -> raise Not_found | [id,p] -> (mkVar id, p) - | (id,p)::_::_ -> if choose then (mkVar id, p) else raise NotUnique + | (id,p)::_::_ -> + if choose then (mkVar id, p) + else raise (NotUniqueInType(find_solution_type (evar_env evi) sols)) in let ty = lazy (Retyping.get_type_of env (evars_of !evdref) t) in let evd = do_projection_effects evar_define env ty !evdref p in @@ -862,14 +888,15 @@ let rec invert_definition choose env evd (evk,argsv as ev) rhs = c with | Not_found -> raise (NotInvertibleUsingOurAlgorithm t) - | NotUnique -> + | NotUniqueInType ty -> if not !progress then raise NotEnoughInformationToProgress; (* No unique projection but still restrict to where it is possible *) let ts = expansions_of_var env t in let test c = isEvar c or List.mem c ts in let filter = array_map_to_list test argsv in let args' = filter_along (fun x -> x) filter argsv in - let evd,evar = do_restrict_hyps_virtual !evdref evk filter in + let evarenv,src,filter,_ = restrict_hyps !evdref evk filter in + let evd,evar = new_evar !evdref evarenv ~src ~filter ty in let evk',_ = destEvar evar in let pb = (Reduction.CONV,env,mkEvar(evk',args'),t) in evdref := Evd.add_conv_pb pb evd; @@ -1122,6 +1149,24 @@ let solve_refl conv_algo env evd evk argsv1 argsv2 = let pb = (Reduction.CONV,env,mkEvar(evk,argsv1),mkEvar(evk,argsv2)) in Evd.add_conv_pb pb evd +(* Util *) + +let check_instance_type conv_algo env evd ev1 t2 = + let t2 = nf_evar (evars_of evd) t2 in + if has_undefined_evars evd t2 then + (* May contain larger constraints than needed: don't want to + commit to an equal solution while only subtyping is requested *) + evd + else + let typ2 = Retyping.get_type_of env (evars_of evd) (refresh_universes t2) in + if isEvar typ2 then (* Don't want to commit too early too *) evd + else + let typ1 = existential_type (evars_of evd) ev1 in + let evd,b = conv_algo env evd Reduction.CUMUL typ2 typ1 in + if b then evd else + user_err_loc (fst (evar_source (fst ev1) evd),"", + str "Unable to find a well-typed instantiation") + (* Tries to solve problem t1 = t2. * Precondition: t1 is an uninstantiated evar * Returns an optional list of evars that were instantiated, or None @@ -1136,15 +1181,23 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1) if evk1 = evk2 then solve_refl conv_algo env evd evk1 args1 args2 else - if pbty = Reduction.CONV + if pbty = None then solve_evar_evar evar_define env evd ev1 ev2 - else add_conv_pb (pbty,env,mkEvar ev1,t2) evd + else if pbty = Some true then + add_conv_pb (Reduction.CUMUL,env,mkEvar ev1,t2) evd + else + add_conv_pb (Reduction.CUMUL,env,t2,mkEvar ev1) evd | _ -> + let evd = + if pbty = Some false then + check_instance_type conv_algo env evd ev1 t2 + else + evd in let evd = evar_define ~choose env ev1 t2 evd in let evm = evars_of evd in let evi = Evd.find evm evk1 in if occur_existential evm evi.evar_concl then - let evenv = evar_env evi in + let evenv = evar_unfiltered_env evi in let evc = nf_isevar evd evi.evar_concl in match evi.evar_body with | Evar_defined body -> diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index cb54f400..eef41da3 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: evarutil.mli 12053 2009-04-06 16:20:42Z msozeau $ i*) +(*i $Id: evarutil.mli 12268 2009-08-11 09:02:16Z herbelin $ i*) (*i*) open Util @@ -80,7 +80,7 @@ val solve_refl : evar_defs val solve_simple_eqn : (env -> evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool) - -> ?choose:bool -> env -> evar_defs -> conv_pb * existential * constr -> + -> ?choose:bool -> env -> evar_defs -> bool option * existential * constr -> evar_defs * bool (* [check_evars env initial_sigma extended_sigma c] fails if some diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 740b2ca8..f579afa6 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacred.ml 11897 2009-02-09 19:28:02Z barras $ *) +(* $Id: tacred.ml 12233 2009-07-08 22:50:56Z herbelin $ *) open Pp open Util @@ -137,20 +137,27 @@ let _ = Summary.survive_module = false; Summary.survive_section = false } -(* Check that c is an "elimination constant" +(* [compute_consteval] determines whether c is an "elimination constant" - either [xn:An]..[x1:A1](

Case (Rel i) of f1..fk end g1 ..gp) + either [yn:Tn]..[y1:T1](match yi with f1..fk end g1 ..gp) - or [xn:An]..[x1:A1](Fix(f|t) (Rel i1) ..(Rel ip)) - with i1..ip distinct variables not occuring in t + or [yn:Tn]..[y1:T1](Fix(f|t) yi1..yip) + with yi1..yip distinct variables among the yi, not occurring in t - In the second case, keep relevenant information ([i1,Ai1;..;ip,Aip],n) - in order to compute an equivalent of Fix(f|t)[xi<-ai] as + In the second case, [check_fix_reversibility [T1;...;Tn] args fix] + checks that [args] is a subset of disjoint variables in y1..yn (a necessary + condition for reversibility). It also returns the relevant + information ([i1,Ti1;..;ip,Tip],n) in order to compute an + equivalent of Fix(f|t) such that - [yip:Bip]..[yi1:Bi1](F bn..b1) - == [yip:Bip]..[yi1:Bi1](Fix(f|t)[xi<-ai] (Rel p)..(Rel 1)) + g := [xp:Tip']..[x1:Ti1'](f a1..an) + == [xp:Tip']..[x1:Ti1'](Fix(f|t) yi1..yip) - with bj=aj if j<>ik and bj=(Rel c) and Bic=Aic[xn..xic-1 <- an..aic-1] + with a_k:=y_k if k<>i_j, a_k:=args_k otherwise, and + Tij':=Tij[x1..xi(j-1) <- a1..ai(j-1)] + + Note that the types Tk, when no i_j=k, must not be dependent on + the xp..x1. *) let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) = @@ -172,8 +179,14 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) = | _ -> raise Elimconst) args in - if not (list_distinct (List.map fst li)) then + let reversible_rels = List.map fst li in + if not (list_distinct reversible_rels) then raise Elimconst; + list_iter_i (fun i t_i -> + if not (List.mem_assoc (i+1) li) then + let fvs = List.map ((+) (i+1)) (Intset.elements (free_rels t_i)) in + if list_intersect fvs reversible_rels <> [] then raise Elimconst) + labs; let k = lv.(i) in if k < nargs then (* Such an optimisation would need eta-expansion @@ -294,19 +307,22 @@ let rev_firstn_liftn fn ln = (* If f is bound to EliminationFix (n',infos), then n' is the minimal number of args for starting the reduction and infos is (nbfix,[(yi1,Ti1);...;(yip,Tip)],n) indicating that f converts - to some [y1:T1,...,yn:Tn](Fix(..) yip .. yi1) where we can remark that - yij = Rel(n+1-j) + to some [y1:T1,...,yn:Tn](Fix(..) yip .. yi1) where the y_{i_j} consist in a + disjoint subset of the yi, i.e. 1 <= ij <= n and the ij are disjoint (in + particular, p <= n). + + f is applied to largs := arg1 .. argn and we need for recursive + calls to build the function - f is applied to largs and we need for recursive calls to build the function g := [xp:Tip',...,x1:Ti1'](f a1 ... an) s.t. (g u1 ... up) reduces to (Fix(..) u1 ... up) This is made possible by setting - a_k:=z_j if k=i_j - a_k:=y_k otherwise + a_k:=x_j if k=i_j for some j + a_k:=arg_k otherwise - The type Tij' is Tij[yn..yi(j-1)..y1 <- ai(j-1)..a1] + The type Tij' is Tij[yi(j-1)..y1 <- ai(j-1)..a1] *) let x = Name (id_of_string "x") @@ -328,7 +344,7 @@ let make_elim_fun (names,(nbfix,lv,n)) largs = | Some (minargs,ref) -> let body = applistc (mkEvalRef ref) la in let g = - list_fold_left_i (fun q (* j from comment is n+1-q *) c (ij,tij) -> + list_fold_left_i (fun q (* j = n+1-q *) c (ij,tij) -> let subst = List.map (lift (-q)) (list_firstn (n-ij) la) in let tij' = substl (List.rev subst) tij in mkLambda (x,tij',c)) 1 body (List.rev lv) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index bfd601e2..c92f1fc6 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: unification.ml 12163 2009-06-06 17:36:47Z herbelin $ *) +(* $Id: unification.ml 12268 2009-08-11 09:02:16Z herbelin $ *) open Pp open Util @@ -517,7 +517,7 @@ let order_metas metas = (* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *) let solve_simple_evar_eqn env evd ev rhs = - let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (CONV,ev,rhs) in + let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (None,ev,rhs) in if not b then error_cannot_unify env (evars_of evd) (mkEvar ev,rhs); let (evd,b) = Evarconv.consider_remaining_unif_problems env evd in if not b then error "Cannot solve unification constraints"; -- cgit v1.2.3