diff options
Diffstat (limited to 'plugins/subtac/subtac_utils.mli')
| -rw-r--r-- | plugins/subtac/subtac_utils.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli index 964f668f2..d60893283 100644 --- a/plugins/subtac/subtac_utils.mli +++ b/plugins/subtac/subtac_utils.mli @@ -24,10 +24,10 @@ val well_founded_ref : global_reference lazy_t val acc_ref : global_reference lazy_t val acc_inv_ref : global_reference lazy_t val fix_sub_ref : global_reference lazy_t +val measure_on_R_ref : global_reference lazy_t val fix_measure_sub_ref : global_reference lazy_t -val lt_ref : global_reference lazy_t -val lt_wf_ref : global_reference lazy_t val refl_ref : global_reference lazy_t +val lt_ref : reference val sig_ref : reference val proj1_sig_ref : reference val proj2_sig_ref : reference |