package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

This file extends Matching with the main logic for Ltac2 match goal.

type match_pattern =
  1. | MatchPattern of Pattern.constr_pattern
  2. | MatchContext of Pattern.constr_pattern
type match_context_hyps = match_pattern

TODO: handle definitions

type match_rule = match_context_hyps list * match_pattern
val match_goal : Environ.env -> Evd.evar_map -> EConstr.constr -> rev:bool -> match_rule -> ((Names.Id.t * context option) list * context option * Ltac_pretype.patvar_map) Proofview.tactic