diff options
| author | Hugo Herbelin | 2014-12-02 21:55:06 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-02 22:39:21 +0100 |
| commit | e1e1a13b015e4963bc5339666c292398298d7bdf (patch) | |
| tree | 95cc03544bc9188987f803ee4d1ccb8e21a635b9 | |
| parent | 801c1c288e1a82a6eeacf7518b2a2a53f4d09c75 (diff) | |
Resolution of evar/evar problems: removed a test which should be
subsumed by the call to project_evar_on_evar.
| -rw-r--r-- | pretyping/evarsolve.ml | 30 |
1 files changed, 12 insertions, 18 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 621174aaa1..ae29318228 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1068,6 +1068,8 @@ let ensure_evar_independent g env evd (evk1,argsv1 as ev1) (evk2,argsv2 as ev2)= exception EvarSolvedOnTheFly of evar_map * constr +(* Try to project evk1[argsv1] on evk2[argsv2], if [ev1] is a pattern on + the common domain of definition *) let project_evar_on_evar g env evd aliases k2 (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) = (* Apply filtering on ev1 so that fvs(ev1) are in fvs(ev2). *) let fvs2 = free_vars_and_rels_up_alias_expansion aliases (mkEvar ev2) in @@ -1113,24 +1115,16 @@ let solve_evar_evar_l2r f g env evd aliases pbty ev1 (evk2,_ as ev2) = f env evd pbty ev2 c let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = - if are_canonical_instances args1 args2 env then - (* If instances are canonical, we solve the problem in linear time *) - let sign = evar_filtered_context (Evd.find evd evk2) in - let id_inst = inst_of_vars sign in - let body = mkEvar(evk1,id_inst) in - let evd' = Evd.define evk2 body evd in - check_evar_instance evd' evk2 body g - else - let evd,ev1,ev2 = - (* If an evar occurs in the instance of the other evar and the - use of an heuristic is forced, we restrict *) - if force then ensure_evar_independent g env evd ev1 ev2 else (evd,ev1,ev2) in - let aliases = make_alias_map env in - try solve_evar_evar_l2r f g env evd aliases pbty ev1 ev2 - with CannotProject filter1 -> - try solve_evar_evar_l2r f g env evd aliases pbty ev2 ev1 - with CannotProject filter2 -> - postpone_evar_evar f env evd pbty filter1 ev1 filter2 ev2 + let evd,ev1,ev2 = + (* If an evar occurs in the instance of the other evar and the + use of an heuristic is forced, we restrict *) + if force then ensure_evar_independent g env evd ev1 ev2 else (evd,ev1,ev2) in + let aliases = make_alias_map env in + try solve_evar_evar_l2r f g env evd aliases pbty ev1 ev2 + with CannotProject filter1 -> + try solve_evar_evar_l2r f g env evd aliases pbty ev2 ev1 + with CannotProject filter2 -> + postpone_evar_evar f env evd pbty filter1 ev1 filter2 ev2 let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = let evi = Evd.find evd evk1 in |