diff options
| author | Erik Martin-Dorel | 2019-03-04 01:25:39 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-04-23 20:22:05 +0200 |
| commit | bb6dc2355bcd027a3a89c40629b82eb2019eff6a (patch) | |
| tree | 97495eceee09a17c9739f8e1db532ccde54e203c /plugins/ssr/ssrcommon.mli | |
| parent | 7c598f9f1f6da2cecc70557f9f436392322fc6d9 (diff) | |
[ssr] under: Add iff support in side-conditions
Diffstat (limited to 'plugins/ssr/ssrcommon.mli')
| -rw-r--r-- | plugins/ssr/ssrcommon.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 3049f67f87..58ce84ecb3 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -349,7 +349,7 @@ val resolve_typeclasses : (*********************** Wrapped Coq tactics *****************************) -val rewritetac : ssrdir -> EConstr.t -> tactic +val rewritetac : ?under:bool -> ssrdir -> EConstr.t -> tactic type name_hint = (int * EConstr.types array) option ref @@ -486,3 +486,4 @@ end val is_ind_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool val is_construct_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool +val is_const_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool |