diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c35109e2c3..8803933e94 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -54,9 +54,9 @@ let rec string_head_bound = function | DOPN(MutInd ind_sp,args) as x -> let mispec = Global.lookup_mind_specif (ind_sp,args) in string_of_id (mis_typename mispec) - | DOPN(MutConstruct ((sp,tyi),i),_) -> - let mib = Global.lookup_mind sp in - string_of_id (mib.mind_packets.(tyi).mind_consnames.(i-1)) + | DOPN(MutConstruct (ind_sp,i),args) -> + let mispec = Global.lookup_mind_specif (ind_sp,args) in + string_of_id (mis_consnames mispec).(i-1) | VAR id -> string_of_id id | _ -> raise Bound |