diff options
Diffstat (limited to 'parsing/g_proofs.ml4')
| -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 7fba1f2799..5acc694aac 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -117,10 +117,12 @@ GEXTEND Gram hints: [ [ IDENT "Resolve"; l = LIST1 global; dbnames = opt_hintbases -> (dbnames, - HintsResolve (List.map (fun qid -> (None, CAppExpl(loc,qid,[]))) l)) + HintsResolve + (List.map (fun qid -> (None, CAppExpl(loc,(false,qid),[]))) l)) | IDENT "Immediate"; l = LIST1 global; dbnames = opt_hintbases -> (dbnames, - HintsImmediate (List.map (fun qid-> (None, CAppExpl (loc,qid,[]))) l)) + HintsImmediate + (List.map (fun qid-> (None, CAppExpl (loc,(false,qid),[]))) l)) | IDENT "Unfold"; l = LIST1 global; dbnames = opt_hintbases -> (dbnames, HintsUnfold (List.map (fun qid -> (None,qid)) l)) ] ] ; |