diff options
| author | Maxime Dénès | 2017-06-06 10:46:33 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-06 10:46:33 +0200 |
| commit | 2f23c27e08f66402b8fba4745681becd402f4c5c (patch) | |
| tree | 8948cdbfa4c908ae9e7f671efbd17744a0e38fc6 /interp/constrintern.mli | |
| parent | 9b44017963a742dacb381a9060f908ce421309fe (diff) | |
| parent | d9ea37641bc67ca269065a9489ec8e70b2f2d246 (diff) | |
Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a short econstr-cleaning of record.ml
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 324f7a3894..a92e94d97b 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -38,7 +38,7 @@ open Misctypes of [env] *) type var_internalization_type = - | Inductive of Id.t list (* list of params *) + | Inductive of Id.t list (* list of params *) * bool (* true = check for possible capture *) | Recursive | Method | Variable @@ -61,7 +61,7 @@ val empty_internalization_env : internalization_env val compute_internalization_data : env -> var_internalization_type -> types -> Impargs.manual_explicitation list -> var_internalization_data -val compute_internalization_env : env -> var_internalization_type -> +val compute_internalization_env : env -> ?impls:internalization_env -> var_internalization_type -> Id.t list -> types list -> Impargs.manual_explicitation list list -> internalization_env |