diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
| commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
| tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /interp/smartlocate.ml | |
| parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff) | |
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/smartlocate.ml')
| -rw-r--r-- | interp/smartlocate.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 07ae87fa0..f16f5363c 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -24,7 +24,7 @@ open Topconstr let global_of_extended_global = function | TrueGlobal ref -> ref - | SynDef kn -> + | SynDef kn -> match search_syntactic_definition dummy_loc kn with | [],ARef ref -> ref | _ -> raise Not_found @@ -33,7 +33,7 @@ let locate_global_with_alias (loc,qid) = let ref = Nametab.locate_extended qid in try global_of_extended_global ref with Not_found -> - user_err_loc (loc,"",pr_qualid qid ++ + user_err_loc (loc,"",pr_qualid qid ++ str " is bound to a notation that does not denote a reference") let global_inductive_with_alias r = |