diff options
Diffstat (limited to 'contrib/correctness')
| -rw-r--r-- | contrib/correctness/pcic.ml | 2 | ||||
| -rw-r--r-- | contrib/correctness/ptactic.ml | 1 |
2 files changed, 2 insertions, 1 deletions
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml index ffcb7c648e..9f28f819f7 100644 --- a/contrib/correctness/pcic.ml +++ b/contrib/correctness/pcic.ml @@ -56,7 +56,7 @@ let tuple_n n = l1n in let cons = id_of_string ("Build_tuple_" ^ string_of_int n) in - Record.definition_structure (false, id, params, fields, cons, mk_Set) + Record.definition_structure ((false, id), params, fields, cons, mk_Set) (*s [(sig_n n)] generates the inductive \begin{verbatim} diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml index d191b58ebf..7bcc3a6579 100644 --- a/contrib/correctness/ptactic.ml +++ b/contrib/correctness/ptactic.ml @@ -229,6 +229,7 @@ let correctness_hook _ ref = register pf_id None let correctness s p opttac = + Library.check_required_module ["Coq";"correctness";"Correctness"]; Pmisc.reset_names(); let p,oc,cty,v = coqast_of_prog p in let env = Global.env () in |