diff options
Diffstat (limited to 'parsing/g_proofs.ml4')
| -rw-r--r-- | parsing/g_proofs.ml4 | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index fdd29feee..5e8d853ee 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -112,7 +112,7 @@ GEXTEND Gram | Coqast.Node(_,"RECCLAUSE",nme::[bd]) -> <:ast<(TACDEF $nme (AST $bd))>> | _ -> - anomalylabstrm "Gram.vernac" [<'sTR "Not a correct RECCLAUSE">]) + anomalylabstrm "Gram.vernac" (str "Not a correct RECCLAUSE")) | IDENT "Recursive"; deftok; "Definition"; vc=vrec_clause; "And"; vcl=LIST1 vrec_clause SEP "And" -> let nvcl= @@ -123,8 +123,10 @@ GEXTEND Gram | Coqast.Node(_,"RECCLAUSE",nme::[bd]) -> nme::<:ast<(AST $bd)>>::b | _ -> - anomalylabstrm "Gram.vernac" [<'sTR - "Not a correct RECCLAUSE">]) (vc::vcl) [] in + anomalylabstrm "Gram.vernac" + (str "Not a correct RECCLAUSE")) + (vc::vcl) [] + in <:ast<(TACDEF ($LIST $nvcl))>> (* Hints for Auto and EAuto *) |