diff options
| author | Gaëtan Gilbert | 2019-05-20 17:11:00 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-06-04 13:58:42 +0200 |
| commit | 99154fcb97653c606d2e62e0a0521c4afddff44c (patch) | |
| tree | 4e8fed2571d370acdc486f486e847a6317d60f69 /plugins/derive | |
| parent | 1ea1e218eed9792685bd7467b63a17fb5ebdbb7e (diff) | |
Rename Proof_global.{pstate -> t}
Diffstat (limited to 'plugins/derive')
| -rw-r--r-- | plugins/derive/derive.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli index 6e4bffa0b6..6bb923118e 100644 --- a/plugins/derive/derive.mli +++ b/plugins/derive/derive.mli @@ -12,4 +12,4 @@ (which can contain references to [f]) in the context extended by [f:=?x]. When the proof ends, [f] is defined as the value of [?x] and [lemma] as the proof. *) -val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> Proof_global.pstate +val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> Proof_global.t |