diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index c19347c4a..463ffa74e 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -95,6 +95,11 @@ and semantic_trigger = and trigger = { content : t list; + (* [content] must be kept sorted in [pat_weight] (see below) order for + matching. + + [mk_trigger] enforces this, but functions that modify [content] and must + preserve this order. *) semantic : semantic_trigger list; hyp : t list; t_depth : int; diff --git a/tests/issues/1111.expected b/tests/issues/1111.expected index e69de29bb..a6e005255 100644 --- a/tests/issues/1111.expected +++ b/tests/issues/1111.expected @@ -0,0 +1,2 @@ + +unknown