diff options
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index e51415abb..45df12e46 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1126,16 +1126,6 @@ let invert_arg evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_e | _ -> res -let effective_projections = - List.map_filter (function Invertible c -> Some c | _ -> None) - -let instance_of_projection f env t evd projs = - let ty = lazy (nf_evar evd (Retyping.get_type_of env evd t)) in - match projs with - | NoUniqueProjection -> raise NotUnique - | UniqueProjection (c,effects) -> - (List.fold_left (do_projection_effects f env ty) evd effects, c) - exception NotEnoughInformationToInvert let extract_unique_projections projs = @@ -1157,8 +1147,6 @@ let extract_candidates sols = with Exit -> None -let filter_of_projection = function Invertible _ -> true | _ -> false - let invert_invertible_arg evd aliases k (evk,argsv) args' = let evi = Evd.find_undefined evd evk in let subst,_ = make_projectable_subst aliases evd evi argsv in @@ -1899,7 +1887,6 @@ let check_evars env initial_sigma sigma c = | _ -> iter_constr proc_rec c in proc_rec c - (****************************************) (* Operations on value/type constraints *) (****************************************) |