diff options
Diffstat (limited to 'src/tac2expr.mli')
| -rw-r--r-- | src/tac2expr.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/tac2expr.mli b/src/tac2expr.mli index 77e2cfef0e..0b9923f7b9 100644 --- a/src/tac2expr.mli +++ b/src/tac2expr.mli @@ -181,7 +181,8 @@ type strexpr = type tag = int type frame = -| FrLtac of ltac_constant option +| FrLtac of ltac_constant +| FrAnon of glb_tacexpr | FrPrim of ml_tactic_name | FrExtn : ('a, 'b) Tac2dyn.Arg.tag * 'b -> frame |