diff options
Diffstat (limited to 'pretyping/pretyping.mli')
| -rw-r--r-- | pretyping/pretyping.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 002e84a49..66ca59152 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -45,9 +45,6 @@ val all_no_fail_flags : inference_flags val all_and_fail_flags : inference_flags -(** Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *) -val allow_anonymous_refs : bool ref - (** Generic calls to the interpreter from glob_constr to open_constr; by default, inference_flags tell to use type classes and heuristics (but no external tactic solver hooks), as well as to |