diff options
Diffstat (limited to 'contrib/subtac/subtac_cases.ml')
| -rw-r--r-- | contrib/subtac/subtac_cases.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index 6a470afc6..45f0f0129 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -1977,7 +1977,7 @@ let build_dependent_signature env evars avoid tomatchs arsign = (lift (nargeqs + nar) arg), mk_eq_refl argt arg) else - (mk_JMeq (lift (nargeqs + slift) appt) + (mk_JMeq (lift (nargeqs + slift) t) (mkRel (nargeqs + slift)) (lift (nargeqs + nar) argt) (lift (nargeqs + nar) arg), |