diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_proofs.ml4 | 6 |
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)) ] ] ; |