From d97cd41db7786ee5172bb00fa2efd1c25ce44a4e Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 31 Oct 2012 17:10:23 +0000
Subject: Change [Hints Resolve] to still accept constrs as arguments to
 maintain compatibility, the term is then declared as a constant internally.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15948 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/smartlocate.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'interp')

diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index adf611b563..c5a28ab2d0 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -25,6 +25,7 @@ let global_of_extended_global = function
   | SynDef kn ->
   match search_syntactic_definition kn with
   | [],NRef ref -> ref
+  | [],NApp (NRef ref,[]) -> ref
   | _ -> raise Not_found
 
 let locate_global_with_alias (loc,qid) =
-- 
cgit v1.2.3