From 0d8a11017e45ff9b0b18af1d6cd69c66184b55ae Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sun, 2 Mar 2014 14:17:09 +0100 Subject: Matching --> ConstrMatching (was clashing with OCaml's compiler-libs) There are currently two other clashs : Lexer and Errors, but for the moment these ones haven't impacted my experiments with extraction and compiler-libs, while this Matching issue had. And anyway the new name is more descriptive, in the spirit of the recent TacticMatching. --- tactics/tacticMatching.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics/tacticMatching.mli') diff --git a/tactics/tacticMatching.mli b/tactics/tacticMatching.mli index 1b440e195..6889ea0e9 100644 --- a/tactics/tacticMatching.mli +++ b/tactics/tacticMatching.mli @@ -17,7 +17,7 @@ those of {!Matching.matching_result}), and a {!Term.constr} substitution mapping corresponding to matched hypotheses. *) type 'a t = { - subst : Matching.bound_ident_map * Pattern.extended_patvar_map ; + subst : ConstrMatching.bound_ident_map * Pattern.extended_patvar_map ; context : Term.constr Names.Id.Map.t; terms : Term.constr Names.Id.Map.t; lhs : 'a; -- cgit v1.2.3