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 Ltac's (lazy)match and (lazy)match goal.

t is the type of matching successes. It ultimately contains a Tacexpr.glob_tactic_expr representing the left-hand side of the corresponding matching rule, a matching substitution to be applied, a context substitution mapping identifier to context like those of Matching.matching_result), and a Term.constr substitution mapping corresponding to matched hypotheses.

match_term env sigma term rules matches the term term with the set of matching rules rules. The environment env and the evar_map sigma are not currently used, but avoid code duplication.

match_goal env sigma hyps concl rules matches the goal hyps|-concl with the set of matching rules rules. The environment env and the evar_map sigma are used to check convertibility for pattern variables shared between hypothesis patterns or the conclusion pattern.