diff options
| author | Hugo Herbelin | 2014-12-02 18:44:01 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-02 22:39:21 +0100 |
| commit | 2aedef1359e2950d2c1c58b4374dbead6e859883 (patch) | |
| tree | 47ee03d9cd7c02bf2a02de8ba1170391e5487f77 /pretyping/evarsolve.ml | |
| parent | e1e1a13b015e4963bc5339666c292398298d7bdf (diff) | |
Being consistent in making arbitrary choices in recursive calls to
evar_define.
Interestingly, the added choose in evarconv.ml allows solve_evar_evar
to be observationally commutative, in the sense of not either fail or
succeed in compiling the stdlib whether problems are given in the
left-to-right or right-to-left order.
Diffstat (limited to 'pretyping/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index ae29318228..b8acd6411e 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1263,7 +1263,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = if choose then (mkVar id, p) else raise (NotUniqueInType sols) in let ty = lazy (Retyping.get_type_of env !evdref t) in - let evd = do_projection_effects (evar_define conv_algo) env ty !evdref p in + let evd = do_projection_effects (evar_define conv_algo ~choose) env ty !evdref p in evdref := evd; c with @@ -1276,7 +1276,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = let ty = find_solution_type (evar_filtered_env evi) sols in let ty' = instantiate_evar_array evi ty argsv in let (evd,evar,(evk',argsv' as ev')) = - materialize_evar (evar_define conv_algo) env !evdref 0 ev ty' in + materialize_evar (evar_define conv_algo ~choose) env !evdref 0 ev ty' in let ts = expansions_of_var aliases t in let test c = isEvar c || List.mem_f Constr.equal c ts in let filter = restrict_upon_filter evd evk test argsv' in @@ -1326,7 +1326,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = (* Make the virtual left evar real *) let ty = get_type_of env' !evdref t in let (evd,evar'',ev'') = - materialize_evar (evar_define conv_algo) env' !evdref k ev ty in + materialize_evar (evar_define conv_algo ~choose) env' !evdref k ev ty in (* materialize_evar may instantiate ev' by another evar; adjust it *) let (evk',args' as ev') = normalize_evar evd ev' in let evd = @@ -1339,7 +1339,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = | EvarSolvedOnTheFly _ -> assert false (* ev has no candidates *) | CannotProject filter'' -> (* ... or postpone the problem *) - postpone_evar_evar (evar_define conv_algo) env' evd None filter'' ev'' filter' ev' in + postpone_evar_evar (evar_define conv_algo ~choose) env' evd None filter'' ev'' filter' ev' in evdref := evd; evar'') | _ -> @@ -1370,7 +1370,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = | [x] -> x | _ -> let (evd,evar'',ev'') = - materialize_evar (evar_define conv_algo) env' !evdref k ev ty in + materialize_evar (evar_define conv_algo ~choose) env' !evdref k ev ty in evdref := restrict_evar evd (fst ev'') None (UpdateWith candidates); evar'') | None -> |