diff options
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 7b77afd07..e662cd41d 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -353,8 +353,8 @@ type ('a,'b) journey_info_tac = (* journey_info : specifies the actions to do on the different term constructors during the travelling of the term *) type journey_info = - { letiN : ((name*constr*types*constr),constr) journey_info_tac; - lambdA : ((name*types*constr),constr) journey_info_tac; + { letiN : ((Name.t*constr*types*constr),constr) journey_info_tac; + lambdA : ((Name.t*types*constr),constr) journey_info_tac; casE : ((constr infos -> tactic) -> constr infos -> tactic) -> ((case_info * constr * constr * constr array),constr) journey_info_tac; otherS : (unit,constr) journey_info_tac; |