diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 4 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e3dba232b2..0cadffa4fe 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -82,7 +82,7 @@ let search_guard loc env possible_indexes fixdefs = iraise (e, info)); indexes else - (* we now search recursively amoungst all combinations *) + (* we now search recursively among all combinations *) (try List.iter (fun l -> @@ -220,7 +220,7 @@ let process_inference_flags flags env initial_sigma (sigma,c) = let c = if flags.expand_evars then nf_evar sigma c else c in sigma,c -(* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) +(* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *) let allow_anonymous_refs = ref false (* Utilisé pour inférer le prédicat des Cases *) diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 7d1e0c9b5b..142b54513e 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -63,7 +63,7 @@ val all_no_fail_flags : inference_flags val all_and_fail_flags : inference_flags -(** Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) +(** Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *) val allow_anonymous_refs : bool ref (** Generic call to the interpreter from glob_constr to open_constr, leaving |