diff options
| author | filliatr | 2001-10-12 07:56:19 +0000 |
|---|---|---|
| committer | filliatr | 2001-10-12 07:56:19 +0000 |
| commit | 2367f109b226070e530f4f05ec644e5fc82ab63e (patch) | |
| tree | d4493dfb65603facf6818973dd715377e5e437f5 /contrib/correctness | |
| parent | 301a70e45eac43f034077c95bce04edbcf2ab4ad (diff) | |
reparation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2110 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/correctness')
| -rw-r--r-- | contrib/correctness/pdb.ml | 2 | ||||
| -rw-r--r-- | contrib/correctness/perror.ml | 2 | ||||
| -rw-r--r-- | contrib/correctness/pmisc.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/contrib/correctness/pdb.ml b/contrib/correctness/pdb.ml index 7ad6a79dba..a0651e90c2 100644 --- a/contrib/correctness/pdb.ml +++ b/contrib/correctness/pdb.ml @@ -19,7 +19,7 @@ open Penv let cci_global id = try - Declare.global_reference CCI id + Declare.global_reference id with _ -> raise Not_found diff --git a/contrib/correctness/perror.ml b/contrib/correctness/perror.ml index 950bc62bfa..1eb44d5bc5 100644 --- a/contrib/correctness/perror.ml +++ b/contrib/correctness/perror.ml @@ -65,7 +65,7 @@ let check_for_array loc id = function let is_constant_type s = function TypePure c -> let id = id_of_string s in - let c' = Declare.global_reference CCI id in + let c' = Declare.global_reference id in Reduction.is_conv (Global.env()) Evd.empty c c' | _ -> false diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml index 936c39d565..60fe808e0f 100644 --- a/contrib/correctness/pmisc.ml +++ b/contrib/correctness/pmisc.ml @@ -151,7 +151,7 @@ let coq_false = mkMutConstruct ((bool_sp,0),2) let constant s = let id = id_of_string s in - Declare.global_reference CCI id + Declare.global_reference id let connective_and = id_of_string "prog_bool_and" let connective_or = id_of_string "prog_bool_or" |