From 2a45c6df8b243ddd3e70e8b5244d1ce8014e7970 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 28 Mar 2018 17:30:02 +0200 Subject: Patterns: Accepting patterns in PFix and PCofix and not only constr. --- intf/pattern.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'intf') 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 *) -- cgit v1.2.3