Utilisation de CAppExpl au lieu de CRef pour les hints pour qu'aucun implicite

ne s'insére pour les références dont tous les arguments sont implicites


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3847 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 2 deletions

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index f6801bf317..7fba1f2799 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -116,9 +116,11 @@ GEXTEND Gram
   ;
   hints:
     [ [ IDENT "Resolve"; l = LIST1 global; dbnames = opt_hintbases ->
-         (dbnames, HintsResolve (List.map (fun qid -> (None, CRef qid)) l))
+         (dbnames, 
+	  HintsResolve (List.map (fun qid -> (None, CAppExpl(loc,qid,[]))) l))
       | IDENT "Immediate"; l = LIST1 global; dbnames = opt_hintbases ->
-        (dbnames, HintsImmediate (List.map (fun qid -> (None, CRef qid)) l))
+        (dbnames, 
+	 HintsImmediate (List.map (fun qid-> (None, CAppExpl (loc,qid,[]))) l))
       | IDENT "Unfold"; l = LIST1 global; dbnames = opt_hintbases ->
         (dbnames, HintsUnfold (List.map (fun qid -> (None,qid)) l)) ] ]
     ;