aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/correctness
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/correctness')
-rw-r--r--contrib/correctness/past.mli2
-rw-r--r--contrib/correctness/pcic.ml11
-rw-r--r--contrib/correctness/pdb.ml25
-rw-r--r--contrib/correctness/penv.ml24
-rw-r--r--contrib/correctness/penv.mli5
-rw-r--r--contrib/correctness/pmisc.ml2
-rw-r--r--contrib/correctness/pmisc.mli2
-rw-r--r--contrib/correctness/psyntax.ml44
-rw-r--r--contrib/correctness/ptactic.ml6
-rw-r--r--contrib/correctness/pwp.ml4
10 files changed, 36 insertions, 49 deletions
diff --git a/contrib/correctness/past.mli b/contrib/correctness/past.mli
index 9919ee993..3c5a56c1d 100644
--- a/contrib/correctness/past.mli
+++ b/contrib/correctness/past.mli
@@ -23,7 +23,7 @@ type variable = identifier
type pattern =
| PatVar of identifier
- | PatConstruct of identifier * ((section_path * int) * int)
+ | PatConstruct of identifier * ((kernel_name * int) * int)
| PatAlias of pattern * identifier
| PatPair of pattern * pattern
| PatApp of pattern list
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index 9f28f819f..30959acda 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -11,6 +11,7 @@
(* $Id$ *)
open Names
+open Libnames
open Term
open Termops
open Nametab
@@ -19,6 +20,7 @@ open Indtypes
open Sign
open Rawterm
open Typeops
+open Entries
open Pmisc
open Past
@@ -33,8 +35,9 @@ let make_hole c = mkCast (isevar, c)
* wether they are dependant (last element only) or not.
* If necessary, tuples are generated ``on the fly''. *)
-let tuple_exists id =
- try let _ = Nametab.sp_of_id id in true with Not_found -> false
+let tuple_exists id =
+ try let _ = Nametab.locate (make_short_qualid id) in true
+ with Not_found -> false
let ast_set = Ast.ope ("SET", [])
@@ -123,13 +126,13 @@ let tuple_ref dep n =
let name = Printf.sprintf "exist_%d" n in
let id = id_of_string name in
if not (tuple_exists id) then ignore (sig_n n);
- Nametab.sp_of_id id
+ Nametab.locate (make_short_qualid id)
end
else begin
let name = Printf.sprintf "Build_tuple_%d" n in
let id = id_of_string name in
if not (tuple_exists id) then tuple_n n;
- Nametab.sp_of_id id
+ Nametab.locate (make_short_qualid id)
end
(* Binders. *)
diff --git a/contrib/correctness/pdb.ml b/contrib/correctness/pdb.ml
index 142ba63c9..3aeb876dd 100644
--- a/contrib/correctness/pdb.ml
+++ b/contrib/correctness/pdb.ml
@@ -87,31 +87,6 @@ let rec db_binders ((tids,pids,refs) as idl) = function
let idl',rem' = db_binders idl rem in idl', a :: rem'
-(* db patterns *)
-
-let rec db_pattern = function
- | (PatVar id) as t ->
- (try
- (match Nametab.sp_of_id id with
- | ConstructRef (x,y) -> [], PatConstruct (id,(x,y))
- | _ -> [id],t)
- with Not_found -> [id],t)
- | PatAlias (p,id) ->
- let ids,p' = db_pattern p in ids,PatAlias (p',id)
- | PatPair (p1,p2) ->
- let ids1,p1' = db_pattern p1 in
- let ids2,p2' = db_pattern p2 in
- ids1@ids2, PatPair (p1',p2')
- | PatApp pl ->
- let ids,pl' =
- List.fold_right
- (fun p (ids,pl) ->
- let ids',p' = db_pattern p in ids'@ids,p'::pl) pl ([],[]) in
- ids,PatApp pl'
- | PatConstruct _ ->
- assert false (* constructor in a pattern after parsing ! *)
-
-
(* db programs *)
let db_prog e =
diff --git a/contrib/correctness/penv.ml b/contrib/correctness/penv.ml
index 9ac7bee8e..568253864 100644
--- a/contrib/correctness/penv.ml
+++ b/contrib/correctness/penv.ml
@@ -111,11 +111,13 @@ let cache_global (_,(id,v,p)) =
env := Env.add id v !env; add_pgm id p
let (inProg,outProg) =
- declare_object ("programs-objects",
- { load_function = cache_global;
- cache_function = cache_global;
- open_function = (fun _ -> ());
- export_function = (fun x -> Some x) })
+ declare_object { object_name = "programs-objects";
+ cache_function = cache_global;
+ load_function = (fun _ -> cache_global);
+ open_function = (fun _ _ -> ());
+ classify_function = (fun _ -> Dispose);
+ subst_function = (fun (_,_,x) -> x);
+ export_function = (fun x -> Some x) }
let is_mutable = function Ref _ | Array _ -> true | _ -> false
@@ -173,11 +175,13 @@ let cache_init (_,(id,c)) =
init_table := Idmap.add id c !init_table
let (inInit,outInit) =
- declare_object ("programs-objects-init",
- { load_function = cache_init;
- open_function = (fun _ -> ());
- cache_function = cache_init;
- export_function = fun x -> Some x })
+ declare_object { object_name = "programs-objects-init";
+ cache_function = cache_init;
+ load_function = (fun _ -> cache_init);
+ open_function = (fun _ _-> ());
+ classify_function = (fun _ -> Dispose);
+ subst_function = (fun (_,_,x) -> x);
+ export_function = fun x -> Some x }
let initialize id c = Lib.add_anonymous_leaf (inInit (id,c))
diff --git a/contrib/correctness/penv.mli b/contrib/correctness/penv.mli
index 83ac2d91a..db6535681 100644
--- a/contrib/correctness/penv.mli
+++ b/contrib/correctness/penv.mli
@@ -13,6 +13,7 @@
open Ptype
open Past
open Names
+open Libnames
open Term
(* Environment for imperative programs.
@@ -45,8 +46,8 @@ type typed_program = (typing_info, constr) t
(* global environment *)
-val add_global : identifier -> type_v -> typed_program option -> section_path
-val add_global_set : identifier -> section_path
+val add_global : identifier -> type_v -> typed_program option -> object_name
+val add_global_set : identifier -> object_name
val is_global : identifier -> bool
val is_global_set : identifier -> bool
val lookup_global : identifier -> type_v
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index bb9f539bb..2772b9f7a 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -145,7 +145,7 @@ let real_subst_in_constr = replace_vars
(* Coq constants *)
let coq_constant d s =
- make_path
+ Libnames.encode_kn
(make_dirpath (List.rev (List.map id_of_string ("Coq"::d))))
(id_of_string s)
diff --git a/contrib/correctness/pmisc.mli b/contrib/correctness/pmisc.mli
index 9e32f147e..393141233 100644
--- a/contrib/correctness/pmisc.mli
+++ b/contrib/correctness/pmisc.mli
@@ -53,7 +53,7 @@ val subst_ast_in_ast : (identifier * Coqast.t) list -> Coqast.t -> Coqast.t
val real_subst_in_constr : (identifier * constr) list -> constr -> constr
val constant : string -> constr
-val coq_constant : string list -> string -> section_path
+val coq_constant : string list -> string -> kernel_name
val conj : constr -> constr -> constr
val coq_true : constr
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 6f07ad93e..59a32bafb 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -547,8 +547,8 @@ let _ =
let v = Ptyping.cic_type_v env ren v in
if not (is_mutable v) then begin
let c =
- Safe_typing.ParameterEntry (trad_ml_type_v ren env v),
- Nametab.NeverDischarge in
+ Entries.ParameterEntry (trad_ml_type_v ren env v),
+ Libnames.NeverDischarge in
List.iter
(fun id -> ignore (Declare.declare_constant id c)) ids;
if_verbose (is_assumed false) ids
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index 1a0d4dc41..aac393690 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -13,6 +13,7 @@
open Pp
open Options
open Names
+open Libnames
open Term
open Pretyping
open Pfedit
@@ -225,7 +226,8 @@ let register id n =
Penv.register id id'
let correctness_hook _ ref =
- let pf_id = Nameops.basename (Nametab.sp_of_global (Global.env()) ref) in
+ let ctx = Global.named_context () in
+ let pf_id = basename (Nametab.sp_of_global (Some ctx) ref) in
register pf_id None
let correctness s p opttac =
@@ -237,7 +239,7 @@ let correctness s p opttac =
let sigma = Evd.empty in
let cty = Reduction.nf_betaiota cty in
let id = id_of_string s in
- start_proof id (false,Nametab.NeverDischarge) sign cty correctness_hook;
+ start_proof id (false, NeverDischarge) sign cty correctness_hook;
Penv.new_edited id (v,p);
if !debug then show_open_subgoals();
deb_mess (str"Pred.red_cci: Reduction..." ++ fnl ());
diff --git a/contrib/correctness/pwp.ml b/contrib/correctness/pwp.ml
index adaafbc68..e390e156d 100644
--- a/contrib/correctness/pwp.ml
+++ b/contrib/correctness/pwp.ml
@@ -12,6 +12,7 @@
open Util
open Names
+open Libnames
open Term
open Termops
open Environ
@@ -114,7 +115,8 @@ let is_bool = function
| TypePure c ->
(match kind_of_term (strip_outer_cast c) with
| Ind op ->
- string_of_id (id_of_global (Global.env()) (IndRef op)) = "bool"
+ let sign = Global.named_context () in
+ string_of_id (id_of_global (Some sign) (IndRef op)) = "bool"
| _ -> false)
| _ -> false
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-02 08:15:12 +0000