From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- tactics/term_dnet.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tactics/term_dnet.ml') diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 753c608a..8bdcc632 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -37,7 +37,7 @@ struct type 't t = | DRel | DSort - | DRef of global_reference + | DRef of GlobRef.t | DCtx of 't * 't (* (binding list, subterm) = Prods and LetIns *) | DLambda of 't * 't | DApp of 't * 't (* binary app *) @@ -290,7 +290,7 @@ struct | Const (c,u) -> Term (DRef (ConstRef c)) | Ind (i,u) -> Term (DRef (IndRef i)) | Construct (c,u)-> Term (DRef (ConstructRef c)) - | Term.Meta _ -> assert false + | Meta _ -> assert false | Evar (i,_) -> let meta = try Evar.Map.find i !metas -- cgit v1.2.3