summaryrefslogtreecommitdiff
path: root/tactics/term_dnet.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/term_dnet.ml')
-rw-r--r--tactics/term_dnet.ml4
1 files changed, 2 insertions, 2 deletions
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