aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-03-28 17:30:02 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-03-28 20:58:24 +0200
commit2a45c6df8b243ddd3e70e8b5244d1ce8014e7970 (patch)
tree48749808f695651cc7d21b313535cf34e4126cf1 /intf
parentca427f04ca477895117d16a78eefd1ed4ad1876f (diff)
Patterns: Accepting patterns in PFix and PCofix and not only constr.
Diffstat (limited to 'intf')
-rw-r--r--intf/pattern.ml5
1 files changed, 2 insertions, 3 deletions
diff --git a/intf/pattern.ml b/intf/pattern.ml
index af2347674..76367b612 100644
--- a/intf/pattern.ml
+++ b/intf/pattern.ml
@@ -10,7 +10,6 @@
open Names
open Globnames
-open Constr
open Misctypes
(** {5 Patterns} *)
@@ -37,8 +36,8 @@ type constr_pattern =
| PIf of constr_pattern * constr_pattern * constr_pattern
| PCase of case_info_pattern * constr_pattern * constr_pattern *
(int * bool list * constr_pattern) list (** index of constructor, nb of args *)
- | PFix of fixpoint
- | PCoFix of cofixpoint
+ | PFix of (int array * int) * (Name.t array * constr_pattern array * constr_pattern array)
+ | PCoFix of int * (Name.t array * constr_pattern array * constr_pattern array)
(** Nota : in a [PCase], the array of branches might be shorter than
expected, denoting the use of a final "_ => _" branch *)