From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Jul 2015 10:36:12 +0200 Subject: Imported Upstream version 8.5~beta2+dfsg --- pretyping/pretyping.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/pretyping.mli') diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 7d1e0c9b..142b5451 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 -- cgit v1.2.3