diff options
| author | Hugo Herbelin | 2014-08-25 17:50:21 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-13 19:12:34 +0200 |
| commit | c72eb85062edea223f5868c67ded99da7954d49a (patch) | |
| tree | 5f4b39c43f41ee6d83b637a6f72c08b233ed451d | |
| parent | 954ae934849d6af88e8b20e6b69cffbb341a3cf9 (diff) | |
English typo in a function name of evarconv.
| -rw-r--r-- | pretyping/evarconv.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index cdb38ecea3..cd55bc26e2 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1084,7 +1084,7 @@ let max_undefined_with_candidates evd = | [] -> None | a::l -> Some (List.last (a::l)) -let rec solve_unconstrained_evars_with_canditates ts evd = +let rec solve_unconstrained_evars_with_candidates ts evd = (* max_undefined is supposed to return the most recent, hence possibly most dependent evar *) match max_undefined_with_candidates evd with @@ -1098,7 +1098,7 @@ let rec solve_unconstrained_evars_with_canditates ts evd = let evd = check_evar_instance evd evk a conv_algo in let evd = Evd.define evk a evd in match reconsider_conv_pbs conv_algo evd with - | Success evd -> solve_unconstrained_evars_with_canditates ts evd + | Success evd -> solve_unconstrained_evars_with_candidates ts evd | UnifFailure _ -> aux l with | IllTypedInstance _ -> aux l @@ -1106,7 +1106,7 @@ let rec solve_unconstrained_evars_with_canditates ts evd = (* List.rev is there to favor most dependent solutions *) (* and favor progress when used with the refine tactics *) let evd = aux (List.rev l) in - solve_unconstrained_evars_with_canditates ts evd + solve_unconstrained_evars_with_candidates ts evd let solve_unconstrained_impossible_cases env evd = Evd.fold_undefined (fun evk ev_info evd' -> @@ -1122,7 +1122,7 @@ let solve_unconstrained_impossible_cases env evd = let consider_remaining_unif_problems env ?(ts=Conv_oracle.get_transp_state (Environ.oracle env)) evd = - let evd = solve_unconstrained_evars_with_canditates ts evd in + let evd = solve_unconstrained_evars_with_candidates ts evd in let rec aux evd pbs progress stuck = match pbs with | (pbty,env,t1,t2 as pb) :: pbs -> |