diff options
| author | Pierre-Marie Pédrot | 2017-09-01 00:57:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-04 15:16:19 +0200 |
| commit | cd3819db675bd42510eac1bd616ca20e33e7d997 (patch) | |
| tree | 47a17c77b523d6dec70f93f60e18523c3e6351e6 /src/tac2expr.mli | |
| parent | 818c49240f2ee6fccd38a556c7e90126606e1837 (diff) | |
Closures now wear the constant they originated from.
Diffstat (limited to 'src/tac2expr.mli')
| -rw-r--r-- | src/tac2expr.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/tac2expr.mli b/src/tac2expr.mli index 1045063cd2..470323e7c7 100644 --- a/src/tac2expr.mli +++ b/src/tac2expr.mli @@ -201,6 +201,8 @@ and closure = { (** Bound variables *) clos_exp : glb_tacexpr; (** Body *) + clos_ref : ltac_constant option; + (** Global constant from which the closure originates *) } type ml_tactic = valexpr list -> valexpr Proofview.tactic |