diff options
| author | Pierre-Marie Pédrot | 2017-09-14 16:07:47 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-14 17:26:35 +0200 |
| commit | 7cee394fc0c6a7a28def2222be0289d6083f47c2 (patch) | |
| tree | 191dc85919a64d1dd0c16642cceb2992a445cb73 /src/tac2expr.mli | |
| parent | 6218f06931384a38445e9d829e6782c069c3ffb4 (diff) | |
Explicit arity for closures.
Diffstat (limited to 'src/tac2expr.mli')
| -rw-r--r-- | src/tac2expr.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/tac2expr.mli b/src/tac2expr.mli index 0b9923f7b9..bbe127e94d 100644 --- a/src/tac2expr.mli +++ b/src/tac2expr.mli @@ -188,6 +188,10 @@ type frame = type backtrace = frame list +type ('a, _) arity = +| OneAty : ('a, 'a -> 'a Proofview.tactic) arity +| AddAty : ('a, 'b) arity -> ('a, 'a -> 'b) arity + type valexpr = | ValInt of int (** Immediate integers *) @@ -202,7 +206,7 @@ type valexpr = | ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr (** Arbitrary data *) -and ml_tactic = valexpr list -> valexpr Proofview.tactic +and ml_tactic = MLTactic : (valexpr, 'v) arity * 'v -> ml_tactic type environment = { env_ist : valexpr Id.Map.t; |