diff options
| author | Gaëtan Gilbert | 2020-02-20 16:31:53 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-03-31 14:39:43 +0200 |
| commit | f19cf4259f63a9c0392c922527e0e9002192949e (patch) | |
| tree | 5f0cf9440e877bf8f1e6b94c13776b8e4060da1d /interp/constrintern.mli | |
| parent | c0a71f9ff6289d99bbbcd13ef65c68f74ac9e191 (diff) | |
Remove check_hidden_implicit_parameters (not needed anymore)
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index fb1c6684a1..9f06f16258 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -38,7 +38,7 @@ open Pretyping of [env] *) type var_internalization_type = - | Inductive of Id.t list (* list of params *) * bool (* true = check for possible capture *) + | Inductive | Recursive | Method | Variable |