diff options
Diffstat (limited to 'parsing/g_proofs.ml4')
| -rw-r--r-- | parsing/g_proofs.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 5b2e165ac..0c9e0ce26 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -124,11 +124,11 @@ GEXTEND Gram [ [ IDENT "Resolve"; l = LIST1 global; dbnames = opt_hintbases -> (dbnames, HintsResolve - (List.map (fun qid -> (None, CAppExpl(loc,(false,qid),[]))) l)) + (List.map (fun qid -> (None, CAppExpl(loc,(None,qid),[]))) l)) | IDENT "Immediate"; l = LIST1 global; dbnames = opt_hintbases -> (dbnames, HintsImmediate - (List.map (fun qid-> (None, CAppExpl (loc,(false,qid),[]))) l)) + (List.map (fun qid-> (None, CAppExpl (loc,(None,qid),[]))) l)) | IDENT "Unfold"; l = LIST1 global; dbnames = opt_hintbases -> (dbnames, HintsUnfold (List.map (fun qid -> (None,qid)) l)) ] ] ; |