aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/auto.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-01-08 18:18:02 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-01-08 19:05:14 +0100
commitd08532d5344d96d10604760fa44109c9d56e73ce (patch)
tree2f5b472f526a6ad9f72cb57bde4503501f9c7129 /tactics/auto.ml
parentb584c5529f7195849b0dd4f1eebf7c73c46f60db (diff)
Avoiding introducing yet another convention in naming files.
Diffstat (limited to 'tactics/auto.ml')
-rw-r--r--tactics/auto.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index ef6c38bf6..fc4a459de 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -129,8 +129,8 @@ let conclPattern concl pat tac =
| None -> Proofview.tclUNIT Id.Map.empty
| Some pat ->
try
- Proofview.tclUNIT (ConstrMatching.matches env sigma pat concl)
- with ConstrMatching.PatternMatchingFailure ->
+ Proofview.tclUNIT (Constr_matching.matches env sigma pat concl)
+ with Constr_matching.PatternMatchingFailure ->
Proofview.tclZERO (UserError ("conclPattern",str"conclPattern"))
in
Proofview.Goal.enter (fun gl ->