diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/clenv.mli | 2 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 2 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 4 |
3 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index 9ad64e31d..b1f08a691 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -28,7 +28,7 @@ open Mod_subst * [templval] is the template which we are trying to fill out. * [templtyp] is its type. * [namenv] is a mapping from metavar numbers to names, for - * use in instanciating metavars by name. + * use in instantiating metavars by name. *) type clausenv = { templenv : env; diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index aec4c2fa3..9f9cc46a6 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -127,7 +127,7 @@ let check_conv_record (t1,l1) (t2,l2) = raise Not_found -(* Precondition: one of the terms of the pb is an uninstanciated evar, +(* Precondition: one of the terms of the pb is an uninstantiated evar, * possibly applied to arguments. *) let rec ise_try isevars = function diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 4f956ffc6..ec8fcd2a8 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -319,7 +319,7 @@ let do_restrict_hyps evd ev args = let need_restriction isevars args = not (array_for_all closed0 args) -(* We try to instanciate the evar assuming the body won't depend +(* We try to instantiate the evar assuming the body won't depend * on arguments that are not Rels or Vars, or appearing several times. *) (* Note: error_not_clean should not be an error: it simply means that the @@ -513,7 +513,7 @@ let solve_refl conv_algo env isevars ev argsv1 argsv2 = (* Tries to solve problem t1 = t2. - * Precondition: t1 is an uninstanciated evar + * Precondition: t1 is an uninstantiated evar * Returns an optional list of evars that were instantiated, or None * if the problem couldn't be solved. *) |