PrefaceTest.v

Set Warnings "-notation-overridden,-parsing".
From Coq Require Export String.
From LF Require Import Preface.
Parameter MISSING: Type. 

Module Check. 

Ltac check_type A B := 
match type of A with 
| context[MISSING] => idtac "Missing:" A  
| ?T => first [unify T B; idtac "Type: ok" | idtac "Type: wrong - should be (" B ")"] 
end. 

Ltac print_manual_grade A := 
match eval compute in A with 
| Some (pair ?S ?C) => 
idtac "Score:"  S; 
match eval compute in C with  
| ""%string => idtac "Comment: None"  
| _ => idtac "Comment:" C 
end 
| None => 
idtac "Score: Ungraded"; 
idtac "Comment: None" 
end. 

End Check.

From LF Require Import Preface.
Import Check.

Goal True.

idtac " ".

idtac "Max points - standard: 0".
idtac "Max points - advanced: 0".
Abort.