diff options
Diffstat (limited to 'tactics/term_dnet.ml')
| -rw-r--r-- | tactics/term_dnet.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index c3132ed6f0..ccd7a818b9 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -289,6 +289,7 @@ struct open TDnet let pat_of_constr c : term_pattern = + let open GlobRef in (* To each evar we associate a unique identifier. *) let metas = ref Evar.Map.empty in let rec pat_of_constr c = match Constr.kind c with |