diff options
Diffstat (limited to 'contrib/correctness/psyntax.mli')
| -rw-r--r-- | contrib/correctness/psyntax.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/contrib/correctness/psyntax.mli b/contrib/correctness/psyntax.mli index f5128fdef..dac571de5 100644 --- a/contrib/correctness/psyntax.mli +++ b/contrib/correctness/psyntax.mli @@ -13,13 +13,14 @@ open Pcoq open Ptype open Past +open Topconstr (* Grammar for the programs and the tactic Correctness *) module Programs : sig val program : program Gram.Entry.e - val type_v : Coqast.t ml_type_v Gram.Entry.e - val type_c : Coqast.t ml_type_c Gram.Entry.e + val type_v : constr_expr ml_type_v Gram.Entry.e + val type_c : constr_expr ml_type_c Gram.Entry.e end |