aboutsummaryrefslogtreecommitdiff
path: root/src/tac2qexpr.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-09-14 00:02:39 +0200
committerPierre-Marie Pédrot2017-09-14 00:08:03 +0200
commit4ed40a9427f67ab6091f1af5457ffdec5e156d12 (patch)
tree1bf8cd68108c066e2a9316f9c2b5761ba94f7902 /src/tac2qexpr.mli
parentc6fb27a363b38c30c7f9953d5f74e9eb98a26387 (diff)
Use a simpler syntax for generalize grammar.
This removes the use for a quotation.
Diffstat (limited to 'src/tac2qexpr.mli')
-rw-r--r--src/tac2qexpr.mli5
1 files changed, 0 insertions, 5 deletions
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index 59c7ad6f3f..7d02022e07 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -139,8 +139,3 @@ type move_location_r =
| QMoveLast
type move_location = move_location_r located
-
-type generalization =
- (Constrexpr.constr_expr * occurrences * Id.t located or_anti option) located
-
-type generalizations = generalization list located