diff options
Diffstat (limited to 'intf/pattern.ml')
| -rw-r--r-- | intf/pattern.ml | 45 |
1 files changed, 3 insertions, 42 deletions
diff --git a/intf/pattern.ml b/intf/pattern.ml index 2ab526984a..64873a0394 100644 --- a/intf/pattern.ml +++ b/intf/pattern.ml @@ -8,52 +8,13 @@ open Names open Globnames -open Term +open Constr open Misctypes -(** {5 Maps of pattern variables} *) - -(** Type [constr_under_binders] is for representing the term resulting - of a matching. Matching can return terms defined in a some context - of named binders; in the context, variable names are ordered by - (<) and referred to by index in the term Thanks to the canonical - ordering, a matching problem like - - [match ... with [(fun x y => ?p,fun y x => ?p)] => [forall x y => p]] - - will be accepted. Thanks to the reference by index, a matching - problem like - - [match ... with [(fun x => ?p)] => [forall x => p]] - - will work even if [x] is also the name of an existing goal - variable. - - Note: we do not keep types in the signature. Besides simplicity, - the main reason is that it would force to close the signature over - binders that occur only in the types of effective binders but not - in the term itself (e.g. for a term [f x] with [f:A -> True] and - [x:A]). - - On the opposite side, by not keeping the types, we loose - opportunity to propagate type informations which otherwise would - not be inferable, as e.g. when matching [forall x, x = 0] with - pattern [forall x, ?h = 0] and using the solution "x|-h:=x" in - expression [forall x, h = x] where nothing tells how the type of x - could be inferred. We also loose the ability of typing ltac - variables before calling the right-hand-side of ltac matching clauses. *) - -type constr_under_binders = Id.t list * EConstr.constr - -(** Types of substitutions with or w/o bound variables *) - -type patvar_map = EConstr.constr Id.Map.t -type extended_patvar_map = constr_under_binders Id.Map.t - (** {5 Patterns} *) type case_info_pattern = - { cip_style : case_style; + { cip_style : Constr.case_style; cip_ind : inductive option; cip_ind_tags : bool list option; (** indicates LetIn/Lambda in arity *) cip_extensible : bool (** does this match end with _ => _ ? *) } @@ -65,7 +26,7 @@ type constr_pattern = | PRel of int | PApp of constr_pattern * constr_pattern array | PSoApp of patvar * constr_pattern list - | PProj of projection * constr_pattern + | PProj of Projection.t * constr_pattern | PLambda of Name.t * constr_pattern * constr_pattern | PProd of Name.t * constr_pattern * constr_pattern | PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern |