diff options
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 30 |
1 files changed, 20 insertions, 10 deletions
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 |