From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- pretyping/evarconv.ml | 415 +++++++++++++++++++++++++++++++------------------- 1 file changed, 255 insertions(+), 160 deletions(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 2264f82b..2b04b693 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -6,20 +6,21 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarconv.ml,v 1.44.6.3 2005/11/29 21:40:52 letouzey Exp $ *) +(* $Id: evarconv.ml 8111 2006-03-02 17:23:41Z herbelin $ *) open Util open Names open Term +open Reduction open Reductionops open Closure -open Instantiate open Environ open Typing open Classops open Recordops open Evarutil open Libnames +open Evd type flex_kind_of_term = | Rigid of constr @@ -69,7 +70,7 @@ let evar_apprec_nobeta env isevars stack c = let (t,stack as s') = apprec_nobeta env (evars_of isevars) s in match kind_of_term t with | Evar (n,_ as ev) when Evd.is_defined (evars_of isevars) n -> - aux (existential_value (evars_of isevars) ev, stack) + aux (Evd.existential_value (evars_of isevars) ev, stack) | _ -> (t, list_of_stack stack) in aux (c, append_stack (Array.of_list stack) empty_stack) *) @@ -77,10 +78,10 @@ let evar_apprec_nobeta env isevars stack c = let evar_apprec env isevars stack c = let sigma = evars_of isevars in let rec aux s = - let (t,stack as s') = Reductionops.apprec env sigma s in + let (t,stack) = Reductionops.apprec env sigma s in match kind_of_term t with | Evar (n,_ as ev) when Evd.is_defined sigma n -> - aux (existential_value sigma ev, stack) + aux (Evd.existential_value sigma ev, stack) | _ -> (t, list_of_stack stack) in aux (c, append_stack (Array.of_list stack) empty_stack) @@ -99,11 +100,11 @@ let apprec_nohdbeta env isevars c = (t2 us2) = (cstr us) extra_args1 = extra_args2 - by finding a record R and an object c := [xs:bs](Build_R a1..am v1..vn) + by finding a record R and an object c := [xs:bs](Build_R params v1..vn) with vi = (cstr us), for which we know that the i-th projection proji satisfies - (proji params c) = (cstr us) + (proji params (c xs)) = (cstr us) Rem: such objects, usable for conversion, are defined in the objdef table; practically, it amounts to "canonically" equip t2 into a @@ -112,10 +113,10 @@ let apprec_nohdbeta env isevars c = let check_conv_record (t1,l1) (t2,l2) = try - let proji = reference_of_constr t1 in - let cstr = reference_of_constr t2 in + let proji = global_of_constr t1 in + let cstr = global_of_constr t2 in let { o_DEF = c; o_TABS = bs; o_TPARAMS = params; o_TCOMPS = us } = - objdef_info (proji, cstr) in + lookup_canonical_conversion (proji, cstr) in let params1, c1, extra_args1 = match list_chop (List.length params) l1 with | params1, c1::extra_args1 -> params1, c1, extra_args1 @@ -126,9 +127,47 @@ let check_conv_record (t1,l1) (t2,l2) = raise Not_found -(* Precondition: one of the terms of the pb is an uninstanciated evar, +(* Precondition: one of the terms of the pb is an uninstantiated evar, * possibly applied to arguments. *) +let rec ise_try isevars = function + [] -> assert false + | [f] -> f isevars + | f1::l -> + let (isevars',b) = f1 isevars in + if b then (isevars',b) else ise_try isevars l + +let ise_and isevars l = + let rec ise_and i = function + [] -> assert false + | [f] -> f i + | f1::l -> + let (i',b) = f1 i in + if b then ise_and i' l else (isevars,false) in + ise_and isevars l + +let ise_list2 isevars f l1 l2 = + let rec ise_list2 i l1 l2 = + match l1,l2 with + [], [] -> (i, true) + | [x], [y] -> f i x y + | x::l1, y::l2 -> + let (i',b) = f i x y in + if b then ise_list2 i' l1 l2 else (isevars,false) + | _ -> (isevars, false) in + ise_list2 isevars l1 l2 + +let ise_array2 isevars f v1 v2 = + let rec allrec i = function + | -1 -> (i,true) + | n -> + let (i',b) = f i v1.(n) v2.(n) in + if b then allrec i' (n-1) else (isevars,false) + in + let lv1 = Array.length v1 in + if lv1 = Array.length v2 then allrec isevars (pred lv1) + else (isevars,false) + let rec evar_conv_x env isevars pbty term1 term2 = let sigma = evars_of isevars in let term1 = whd_castappevar sigma term1 in @@ -138,15 +177,15 @@ let rec evar_conv_x env isevars pbty term1 term2 = true else *) - (* Maybe convertible but since reducing can erase evars which [evar_apprec]*) - (* could have found, we do it only if the terms are free of evar *) - (not (has_undefined_isevars isevars term1) & - not (has_undefined_isevars isevars term2) & - is_fconv pbty env (evars_of isevars) term1 term2) - or - if ise_undefined isevars term1 then + (* Maybe convertible but since reducing can erase evars which [evar_apprec] + could have found, we do it only if the terms are free of evar. + Note: incomplete heuristic... *) + if is_ground_term isevars term1 && is_ground_term isevars term2 & + is_fconv pbty env (evars_of isevars) term1 term2 then + (isevars,true) + else if is_undefined_evar isevars term1 then solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term1,term2) - else if ise_undefined isevars term2 then + else if is_undefined_evar isevars term2 then solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term2,term1) else let (t1,l1) = apprec_nohdbeta env isevars term1 in @@ -154,7 +193,7 @@ let rec evar_conv_x env isevars pbty term1 term2 = if (head_is_embedded_evar isevars t1 & not(is_eliminator t2)) or (head_is_embedded_evar isevars t2 & not(is_eliminator t1)) then - (add_conv_pb isevars (pbty,applist(t1,l1),applist(t2,l2)); true) + (add_conv_pb (pbty,applist(t1,l1),applist(t2,l2)) isevars, true) else evar_eqappr_x env isevars pbty (t1,l1) (t2,l2) @@ -162,67 +201,81 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = (* Evar must be undefined since we have whd_ised *) match (flex_kind_of_term term1 l1, flex_kind_of_term term2 l2) with | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> - let f1 () = + let f1 i = if List.length l1 > List.length l2 then let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in - solve_simple_eqn evar_conv_x env isevars - (pbty,ev2,applist(term1,deb1)) - & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2 + ise_and i + [(fun i -> solve_simple_eqn evar_conv_x env i + (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 - solve_simple_eqn evar_conv_x env isevars - (pbty,ev1,applist(term2,deb2)) - & list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2 - and f2 () = - (sp1 = sp2) - & (array_for_all2 (evar_conv_x env isevars CONV) al1 al2) - & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2) + ise_and i + [(fun i -> solve_simple_eqn evar_conv_x env i + (pbty,ev1,applist(term2,deb2))); + (fun i -> ise_list2 i + (fun i -> evar_conv_x env i CONV) l1 rest2)] + and f2 i = + if sp1 = sp2 then + ise_and i + [(fun i -> ise_array2 i + (fun i -> evar_conv_x env i CONV) al1 al2); + (fun i -> ise_list2 i + (fun i -> evar_conv_x env i CONV) l1 l2)] + else (i,false) in ise_try isevars [f1; f2] | Flexible ev1, MaybeFlexible flex2 -> - let f1 () = - (List.length l1 <= List.length l2) & - let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in - (* First compare extra args for better failure message *) - list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2 & - evar_conv_x env isevars pbty term1 (applist(term2,deb2)) - and f4 () = + let f1 i = + if List.length l1 <= List.length l2 then + let (deb2,rest2) = + list_chop (List.length l2-List.length l1) l2 in + ise_and i + (* First compare extra args for better failure message *) + [(fun i -> ise_list2 i + (fun i -> evar_conv_x env i CONV) l1 rest2); + (fun i -> evar_conv_x env i pbty term1 (applist(term2,deb2)))] + else (i,false) + and f4 i = match eval_flexible_term env flex2 with | Some v2 -> - evar_eqappr_x env isevars pbty - appr1 (evar_apprec env isevars l2 v2) - | None -> false + evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2) + | None -> (i,false) in ise_try isevars [f1; f4] | MaybeFlexible flex1, Flexible ev2 -> - let f1 () = - (List.length l2 <= List.length l1) & - let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in - (* First compare extra args for better failure message *) - list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2 & - evar_conv_x env isevars pbty (applist(term1,deb1)) term2 - and f4 () = + let f1 i = + if List.length l2 <= List.length l1 then + let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in + ise_and i + (* First compare extra args for better failure message *) + [(fun i -> ise_list2 i + (fun i -> evar_conv_x env i CONV) rest1 l2); + (fun i -> evar_conv_x env i pbty (applist(term1,deb1)) term2)] + else (i,false) + and f4 i = match eval_flexible_term env flex1 with | Some v1 -> - evar_eqappr_x env isevars pbty - (evar_apprec env isevars l1 v1) appr2 - | None -> false + evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2 + | None -> (i,false) in ise_try isevars [f1; f4] | MaybeFlexible flex1, MaybeFlexible flex2 -> - let f2 () = - (flex1 = flex2) - & (List.length l1 = List.length l2) - & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2) - and f3 () = - (try conv_record env isevars + let f2 i = + if flex1 = flex2 then + ise_list2 i (fun i -> evar_conv_x env i CONV) l1 l2 + else (i,false) + and f3 i = + (try conv_record env i (try check_conv_record appr1 appr2 with Not_found -> check_conv_record appr2 appr1) - with _ -> false) - and f4 () = +(* TODO: remove this _ !!! *) + with _ -> (i,false)) + and f4 i = (* heuristic: unfold second argument first, exception made if the first argument is a beta-redex (expand a constant only if necessary) *) @@ -232,87 +285,98 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = | _ -> eval_flexible_term env flex2 in match val2 with | Some v2 -> - evar_eqappr_x env isevars pbty - appr1 (evar_apprec env isevars l2 v2) + evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2) | None -> match eval_flexible_term env flex1 with | Some v1 -> - evar_eqappr_x env isevars pbty - (evar_apprec env isevars l1 v1) appr2 - | None -> false + evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2 + | None -> (i,false) in ise_try isevars [f2; f3; f4] | Flexible ev1, Rigid _ -> - (List.length l1 <= List.length l2) & - let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in - (* First compare extra args for better failure message *) - list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2 & - solve_simple_eqn evar_conv_x env isevars - (pbty,ev1,applist(term2,deb2)) - + if (List.length l1 <= List.length l2) then + let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in + ise_and isevars + (* First compare extra args for better failure message *) + [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) l1 rest2); + (fun i -> + (* Then instantiate evar unless already done by unifying args *) + let t2 = applist(term2,deb2) in + if is_defined_evar i ev1 then + evar_conv_x env i pbty (mkEvar ev1) t2 + else + solve_simple_eqn evar_conv_x env i (pbty,ev1,t2))] + else (isevars,false) | Rigid _, Flexible ev2 -> - (List.length l2 <= List.length l1) & - let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in - (* First compare extra args for better failure message *) - list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2 & - solve_simple_eqn evar_conv_x env isevars - (pbty,ev2,applist(term1,deb1)) - + if List.length l2 <= List.length l1 then + let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in + ise_and isevars + (* First compare extra args for better failure message *) + [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest1 l2); + (fun i -> + (* Then instantiate evar unless already done by unifying args *) + let t1 = applist(term1,deb1) in + if is_defined_evar i ev2 then + evar_conv_x env i pbty t1 (mkEvar ev2) + else + solve_simple_eqn evar_conv_x env i (pbty,ev2,t1))] + else (isevars,false) | MaybeFlexible flex1, Rigid _ -> - let f3 () = - (try conv_record env isevars (check_conv_record appr1 appr2) - with _ -> false) - and f4 () = + let f3 i = + (try conv_record env i (check_conv_record appr1 appr2) + with _ -> (i,false)) + and f4 i = match eval_flexible_term env flex1 with | Some v1 -> - evar_eqappr_x env isevars pbty - (evar_apprec env isevars l1 v1) appr2 - | None -> false + evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2 + | None -> (i,false) in ise_try isevars [f3; f4] | Rigid _ , MaybeFlexible flex2 -> - let f3 () = - (try (conv_record env isevars (check_conv_record appr2 appr1)) - with _ -> false) - and f4 () = + let f3 i = + (try (conv_record env i (check_conv_record appr2 appr1)) + with _ -> (i,false)) + and f4 i = match eval_flexible_term env flex2 with | Some v2 -> - evar_eqappr_x env isevars pbty - appr1 (evar_apprec env isevars l2 v2) - | None -> false + evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2) + | None -> (i,false) in ise_try isevars [f3; f4] | Rigid c1, Rigid c2 -> match kind_of_term c1, kind_of_term c2 with - | Cast (c1,_), _ -> evar_eqappr_x env isevars pbty (c1,l1) appr2 + | Cast (c1,_,_), _ -> evar_eqappr_x env isevars pbty (c1,l1) appr2 - | _, Cast (c2,_) -> evar_eqappr_x env isevars pbty appr1 (c2,l2) + | _, Cast (c2,_,_) -> evar_eqappr_x env isevars pbty appr1 (c2,l2) - | Sort s1, Sort s2 when l1=[] & l2=[] -> base_sort_cmp pbty s1 s2 + | Sort s1, Sort s2 when l1=[] & l2=[] -> + (isevars,base_sort_cmp pbty s1 s2) | Lambda (na,c1,c'1), Lambda (_,c2,c'2) when l1=[] & l2=[] -> - evar_conv_x env isevars CONV c1 c2 - & - (let c = nf_evar (evars_of isevars) c1 in - evar_conv_x (push_rel (na,None,c) env) isevars CONV c'1 c'2) + ise_and isevars + [(fun i -> evar_conv_x env i CONV c1 c2); + (fun i -> + let c = nf_evar (evars_of i) c1 in + evar_conv_x (push_rel (na,None,c) env) i CONV c'1 c'2)] | LetIn (na,b1,t1,c'1), LetIn (_,b2,_,c'2) -> - let f1 () = - evar_conv_x env isevars CONV b1 b2 - & - (let b = nf_evar (evars_of isevars) b1 in - let t = nf_evar (evars_of isevars) t1 in - evar_conv_x (push_rel (na,Some b,t) env) isevars pbty c'1 c'2) - & (List.length l1 = List.length l2) - & (List.for_all2 (evar_conv_x env isevars CONV) l1 l2) - and f2 () = - let appr1 = evar_apprec env isevars l1 (subst1 b1 c'1) - and appr2 = evar_apprec env isevars l2 (subst1 b2 c'2) - in evar_eqappr_x env isevars pbty appr1 appr2 + let f1 i = + ise_and i + [(fun i -> evar_conv_x env i CONV b1 b2); + (fun i -> + let b = nf_evar (evars_of i) b1 in + let t = nf_evar (evars_of i) t1 in + evar_conv_x (push_rel (na,Some b,t) env) i pbty c'1 c'2); + (fun i -> ise_list2 i + (fun i -> evar_conv_x env i CONV) l1 l2)] + and f2 i = + let appr1 = evar_apprec env i l1 (subst1 b1 c'1) + and appr2 = evar_apprec env i l2 (subst1 b2 c'2) + in evar_eqappr_x env i pbty appr1 appr2 in ise_try isevars [f1; f2] @@ -325,71 +389,102 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = in evar_eqappr_x env isevars pbty appr1 appr2 | Prod (n,c1,c'1), Prod (_,c2,c'2) when l1=[] & l2=[] -> - evar_conv_x env isevars CONV c1 c2 - & - (let c = nf_evar (evars_of isevars) c1 in - evar_conv_x (push_rel (n,None,c) env) isevars pbty c'1 c'2) + ise_and isevars + [(fun i -> evar_conv_x env i CONV c1 c2); + (fun i -> + let c = nf_evar (evars_of i) c1 in + evar_conv_x (push_rel (n,None,c) env) i pbty c'1 c'2)] | Ind sp1, Ind sp2 -> - sp1=sp2 - & list_for_all2eq (evar_conv_x env isevars CONV) l1 l2 - + if sp1=sp2 then + ise_list2 isevars (fun i -> evar_conv_x env i CONV) l1 l2 + else (isevars, false) + | Construct sp1, Construct sp2 -> - sp1=sp2 - & list_for_all2eq (evar_conv_x env isevars CONV) l1 l2 + if sp1=sp2 then + ise_list2 isevars (fun i -> evar_conv_x env i CONV) l1 l2 + else (isevars, false) | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) -> - evar_conv_x env isevars CONV p1 p2 - & evar_conv_x env isevars CONV c1 c2 - & (array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2) - & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2) + ise_and isevars + [(fun i -> evar_conv_x env i CONV p1 p2); + (fun i -> evar_conv_x env i CONV c1 c2); + (fun i -> ise_array2 i + (fun i -> evar_conv_x env i CONV) cl1 cl2); + (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) l1 l2)] | Fix (li1,(_,tys1,bds1 as recdef1)), Fix (li2,(_,tys2,bds2)) -> - li1=li2 - & (array_for_all2 (evar_conv_x env isevars CONV) tys1 tys2) - & (array_for_all2 - (evar_conv_x (push_rec_types recdef1 env) isevars CONV) - bds1 bds2) - & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2) - + if li1=li2 then + ise_and isevars + [(fun i -> ise_array2 i + (fun i -> evar_conv_x env i CONV) tys1 tys2); + (fun i -> ise_array2 i + (fun i -> evar_conv_x (push_rec_types recdef1 env) i CONV) + bds1 bds2); + (fun i -> ise_list2 i + (fun i -> evar_conv_x env i CONV) l1 l2)] + else (isevars,false) | CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) -> - i1=i2 - & (array_for_all2 (evar_conv_x env isevars CONV) tys1 tys2) - & (array_for_all2 - (evar_conv_x (push_rec_types recdef1 env) isevars CONV) - bds1 bds2) - & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2) - - | (Meta _ | Lambda _), _ -> false - | _, (Meta _ | Lambda _) -> false - - | (Ind _ | Construct _ | Sort _ | Prod _), _ -> false - | _, (Ind _ | Construct _ | Sort _ | Prod _) -> false + if i1=i2 then + ise_and isevars + [(fun i -> ise_array2 i + (fun i -> evar_conv_x env i CONV) tys1 tys2); + (fun i -> ise_array2 i + (fun i -> evar_conv_x (push_rec_types recdef1 env) i CONV) + bds1 bds2); + (fun i -> ise_list2 i + (fun i -> evar_conv_x env i CONV) l1 l2)] + else (isevars,false) + + | (Meta _ | Lambda _), _ -> (isevars,false) + | _, (Meta _ | Lambda _) -> (isevars,false) + + | (Ind _ | Construct _ | Sort _ | Prod _), _ -> (isevars,false) + | _, (Ind _ | Construct _ | Sort _ | Prod _) -> (isevars,false) | (App _ | Case _ | Fix _ | CoFix _), - (App _ | Case _ | Fix _ | CoFix _) -> false + (App _ | Case _ | Fix _ | CoFix _) -> (isevars,false) | (Rel _ | Var _ | Const _ | Evar _), _ -> assert false | _, (Rel _ | Var _ | Const _ | Evar _) -> assert false and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) = - let ks = + let (isevars',ks) = List.fold_left - (fun ks b -> - let dloc = (dummy_loc,Rawterm.InternalHole) in - (new_isevar isevars env dloc (substl ks b)) :: ks) - [] bs + (fun (i,ks) b -> + let dloc = (dummy_loc,InternalHole) in + let (i',ev) = new_evar i env ~src:dloc (substl ks b) in + (i', ev :: ks)) + (isevars,[]) bs in - (list_for_all2eq - (fun u1 u -> evar_conv_x env isevars CONV u1 (substl ks u)) - us2 us) - & - (list_for_all2eq - (fun x1 x -> evar_conv_x env isevars CONV x1 (substl ks x)) - params1 params) - & (list_for_all2eq (evar_conv_x env isevars CONV) ts ts1) - & (evar_conv_x env isevars CONV c1 (applist (c,(List.rev ks)))) + ise_and isevars' + [(fun i -> + ise_list2 i + (fun i u1 u -> evar_conv_x env i CONV u1 (substl ks u)) + us2 us); + (fun i -> + ise_list2 i + (fun i x1 x -> evar_conv_x env i CONV x1 (substl ks x)) + params1 params); + (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) ts ts1); + (fun i -> evar_conv_x env i CONV c1 (applist (c,(List.rev ks))))] -let the_conv_x env isevars t1 t2 = evar_conv_x env isevars CONV t1 t2 -let the_conv_x_leq env isevars t1 t2 = evar_conv_x env isevars CUMUL t1 t2 +let the_conv_x env t1 t2 isevars = + match evar_conv_x env isevars CONV t1 t2 with + (evd',true) -> evd' + | _ -> raise Reduction.NotConvertible + +let the_conv_x_leq env t1 t2 isevars = + match evar_conv_x env isevars CUMUL t1 t2 with + (evd', true) -> evd' + | _ -> raise Reduction.NotConvertible +let e_conv env isevars t1 t2 = + match evar_conv_x env !isevars CONV t1 t2 with + (evd',true) -> isevars := evd'; true + | _ -> false + +let e_cumul env isevars t1 t2 = + match evar_conv_x env !isevars CUMUL t1 t2 with + (evd',true) -> isevars := evd'; true + | _ -> false -- cgit v1.2.3