diff options
Diffstat (limited to 'plugins/funind/merge.ml')
| -rw-r--r-- | plugins/funind/merge.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 3b3f3057b6..3ea9c3d3e7 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -49,7 +49,7 @@ let rec substitterm prof t by_t in_u = let lift_ldecl n ldecl = List.map (fun (x,y) -> x,lift n y) ldecl -let understand = Pretyping.Default.understand Evd.empty (Global.env()) +let understand = Pretyping.understand Evd.empty (Global.env()) (** Operations on names and identifiers *) let id_of_name = function |