diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-09-15 16:57:57 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-08-01 17:19:17 +0200 |
| commit | 9d5b26370a530be4267d07c5bd6e7cf4618f0e4b (patch) | |
| tree | 39471ef6adc0edce4e76abe24ebb06e4e0c9a6d3 /pretyping/pretyping.mli | |
| parent | cd0a6070d9627cdf335c4be0a03b9bbb81f7a738 (diff) | |
Remove allow_anonymous_refs.
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 |