From 392300a73bc4e57d2be865d9a8d77c608ef02f59 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 29 May 2012 11:08:50 +0000 Subject: New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/auto.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics/auto.ml') diff --git a/tactics/auto.ml b/tactics/auto.ml index f167a91a30..f580f839c2 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -825,7 +825,7 @@ let prepare_hint env (sigma,c) = let path_of_constr_expr c = match c with - | Topconstr.CRef r -> (try PathHints [global r] with _ -> PathAny) + | Constrexpr.CRef r -> (try PathHints [global r] with _ -> PathAny) | _ -> PathAny let interp_hints h = -- cgit v1.2.3