aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-09-15 16:53:23 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-08-01 17:03:17 +0200
commitcd0a6070d9627cdf335c4be0a03b9bbb81f7a738 (patch)
tree4b8b36310b93b076eb91e8af0699804f4aa452d6 /pretyping/pretyping.ml
parentba0975d00f49684e33f763e171f9578a702eec85 (diff)
Remove pure_open_constr (now open_constr)
Diffstat (limited to 'pretyping/pretyping.ml')
-rw-r--r--pretyping/pretyping.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 3fae20bcb..32daa0d89 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -47,7 +47,6 @@ open Misctypes
module NamedDecl = Context.Named.Declaration
type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
-type pure_open_constr = evar_map * EConstr.constr
(************************************************************************)
(* This concerns Cases *)