From d2f0b8dd4cb352d95f682c8aea04063ef8e0a973 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 7 Apr 2003 08:32:40 +0000
Subject: 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
---
 parsing/g_proofs.ml4 | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'parsing')

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)) ] ]
     ;
-- 
cgit v1.2.3