diff options
| author | Pierre-Marie Pédrot | 2017-08-08 12:32:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-08 12:42:02 +0200 |
| commit | 3d1092cf7df3229ecc2a4da60a33cf7c6b9be1a3 (patch) | |
| tree | 5d301c0b226a6520bb79026514e5e0bec616c47e /src/tac2qexpr.mli | |
| parent | 5062231251d58cf51cedb18677392b6e6d168694 (diff) | |
Code simplification in quotations.
Diffstat (limited to 'src/tac2qexpr.mli')
| -rw-r--r-- | src/tac2qexpr.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli index f6b8c2c19b..d5520c54ee 100644 --- a/src/tac2qexpr.mli +++ b/src/tac2qexpr.mli @@ -60,9 +60,11 @@ type occurrences = type hyp_location = (occurrences * Id.t located or_anti) * Locus.hyp_location_flag -type clause = +type clause_r = { q_onhyps : hyp_location list option; q_concl_occs : occurrences; } +type clause = clause_r located + type constr_with_bindings = (Constrexpr.constr_expr * bindings) located type destruction_arg = |