diff options
Diffstat (limited to 'grammar/q_constr.ml4')
| -rw-r--r-- | grammar/q_constr.ml4 | 12 |
1 files changed, 3 insertions, 9 deletions
diff --git a/grammar/q_constr.ml4 b/grammar/q_constr.ml4 index f4d3c41f6..8943b2b63 100644 --- a/grammar/q_constr.ml4 +++ b/grammar/q_constr.ml4 @@ -8,16 +8,10 @@ (*i camlp4deps: "tools/compat5b.cmo" i*) -open Glob_term -open Term -open Names -open Pattern open Q_util -open Pp open Compat open Pcaml open PcamlSig -open Misctypes let loc = Loc.ghost let dloc = <:expr< Loc.ghost >> @@ -34,9 +28,9 @@ EXTEND <:expr< snd (Patternops.pattern_of_glob_constr $c$) >> ] ] ; sort: - [ [ "Set" -> GSet - | "Prop" -> GProp - | "Type" -> GType None ] ] + [ [ "Set" -> Misctypes.GSet + | "Prop" -> Misctypes.GProp + | "Type" -> Misctypes.GType None ] ] ; ident: [ [ s = string -> <:expr< Names.id_of_string $str:s$ >> ] ] |