Equality configuration.

get_eq_config ss pos returns the current configuration for equality, used by tactics such as “rewrite” or “reflexivity”.

get_eq_data pos cfg a returns ((a,l,r),[v1;..;vn]) if a ≡ Π v1:A1, .., Π vn:An, P (eq a l r) and fails otherwise.

Type of a term with the free variables that need to be substituted. It is usually used to store the LHS of a proof of equality, together with the variables that were quantified over.

matches p t instantiates the TRef's of p so that p gets equal to t and returns true if all TRef's of p could be instantiated, and false otherwise.

matching_subs (xs,p) t attempts to match the pattern p containing the variables xs) with the term t. If successful, it returns Some ts where ts is an array of terms such that substituting xs by the corresponding elements of ts in p yields t.

WARNING: Some elements of ts may be uninstantiated TRef's. It will happen if not all vars are in LibTerm.free_vars p, for instance when some vars are type variables not occurring in p, for instance when trying to apply an equation of the form x = ... with x of polymorphic type. This could be improved by generating p_terms instead of terms. Indeed, in this case, we could replace uninstantiated TRef's by underscores.

check_subs vars ts check that no element of ts is an uninstantiated TRef.

replace_wild_by_tref t substitutes every wildcard of t by a fresh TRef.

bind_pattern p t replaces in the term t every occurence of the pattern p by a fresh variable, and returns the binder on this variable.

swap cfg a r l t returns a term of type P (eq a l r) from a term t of type P (eq a r l).

rewrite ss p pos gt l2r pat t generates a term for the refine tactic representing the application of the rewrite tactic to the goal type gt. Every occurrence of the first instance of the left-hand side is replaced by the right-hand side of the obtained proof (or the reverse if l2r is false). pat is an optional SSReflect pattern. t is the equational lemma that is appied. It handles the full set of SSReflect patterns.