blob: 588a1a3eac15d067042e79d95c060c062400ee05 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
open Genarg
open Ssrmatching
(** CS cpattern: (f _), (X in t), (t in X in t), (t as X in t) *)
val cpattern : cpattern Pcoq.Entry.t
val wit_cpattern : cpattern uniform_genarg_type
(** OS cpattern: f _, (X in t), (t in X in t), (t as X in t) *)
val lcpattern : cpattern Pcoq.Entry.t
val wit_lcpattern : cpattern uniform_genarg_type
(** OS rpattern: f _, in t, X in t, in X in t, t in X in t, t as X in t *)
val rpattern : rpattern Pcoq.Entry.t
val wit_rpattern : rpattern uniform_genarg_type
|
