diff options
| author | herbelin | 2002-06-03 10:09:53 +0000 |
|---|---|---|
| committer | herbelin | 2002-06-03 10:09:53 +0000 |
| commit | 8a1550e2db6e95004eda1beec57200e214e91c72 (patch) | |
| tree | a4a5f1b8ffbb49bda42a0c767044eea87223ba94 /contrib/correctness | |
| parent | d03d9d2993b4e9e67c3d21f0e4515256917906e1 (diff) | |
Protection des tactiques contre l'utilisation sans le bon contexte de thories
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2745 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |