aboutsummaryrefslogtreecommitdiff
path: root/contrib/interface
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface')
-rw-r--r--contrib/interface/showproof.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 5b265ec864..2560b0b820 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1556,7 +1556,7 @@ and mind_ind_info_hyp_constr indf c =
let env = Global.env() in
let (ind,_) = dest_ind_family indf in
let (mib,mip) = lookup_mind_specif env ind in
- let p = mip.mind_nparams in
+ let p = mib.mind_nparams in
let a = arity_of_constr_of_mind env indf c in
let lp=ref (get_constructors env indf).(c).cs_args in
let lr=ref [] in