diff options
| author | Pierre-Marie Pédrot | 2017-08-04 15:48:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-04 15:51:03 +0200 |
| commit | 2e01ea9e1ab0f9e8d90dd4e4ac598bc1691b9272 (patch) | |
| tree | 73edd9be901385c861cf004876fb862adf771496 /src/tac2qexpr.mli | |
| parent | fce4a1a9cbb57a636155181898ae4ecece5af59d (diff) | |
More precise type for quoted structures.
Diffstat (limited to 'src/tac2qexpr.mli')
| -rw-r--r-- | src/tac2qexpr.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli index 5075f2d7d4..8a61590a1d 100644 --- a/src/tac2qexpr.mli +++ b/src/tac2qexpr.mli @@ -19,8 +19,8 @@ type 'a or_anti = | QAnti of Id.t located type bindings = -| QImplicitBindings of raw_tacexpr list -| QExplicitBindings of (Misctypes.quantified_hypothesis or_anti * raw_tacexpr) Loc.located list +| QImplicitBindings of Constrexpr.constr_expr list +| QExplicitBindings of (Misctypes.quantified_hypothesis or_anti * Constrexpr.constr_expr) Loc.located list | QNoBindings type intro_pattern = |