aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/correctness/pcic.ml2
-rw-r--r--contrib/correctness/pmisc.ml15
-rw-r--r--contrib/correctness/psyntax.ml42
-rw-r--r--contrib/extraction/extract_env.ml9
-rw-r--r--contrib/extraction/haskell.ml3
-rw-r--r--contrib/extraction/ocaml.ml5
-rw-r--r--contrib/extraction/ocaml.mli4
-rw-r--r--contrib/field/field.ml44
-rw-r--r--contrib/omega/coq_omega.ml4
-rw-r--r--contrib/ring/Setoid_ring_normalize.v2
-rw-r--r--contrib/ring/quote.ml2
-rw-r--r--contrib/ring/ring.ml2
-rw-r--r--contrib/xml/xmlcommand.ml24
13 files changed, 41 insertions, 37 deletions
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index ecc17253a..d13be7720 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -48,7 +48,7 @@ let tuple_n n =
(fun i ->
let id = id_of_string
("proj_" ^ string_of_int n ^ "_" ^ string_of_int i) in
- (false, (id, true, Ast.nvar ("T" ^ string_of_int i))))
+ (false, (id, true, Ast.nvar (id_of_string ("T" ^ string_of_int i)))))
l1n
in
let cons = id_of_string ("Build_tuple_" ^ string_of_int n) in
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index d6a15959b..c885242bd 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -120,23 +120,19 @@ let subst_in_constr alist =
replace_vars alist'
let subst_in_ast alist ast =
- let alist' =
- List.map (fun (id,id') -> (string_of_id id,string_of_id id')) alist in
let rec subst = function
- Nvar(l,s) -> Nvar(l,try List.assoc s alist' with Not_found -> s)
+ Nvar(l,s) -> Nvar(l,try List.assoc s alist with Not_found -> s)
| Node(l,s,args) -> Node(l,s,List.map subst args)
- | Slam(l,so,a) -> Slam(l,so,subst a) (* TODO:enlever so de alist' ? *)
+ | Slam(l,so,a) -> Slam(l,so,subst a) (* TODO:enlever so de alist ? *)
| x -> x
in
subst ast
let subst_ast_in_ast alist ast =
- let alist' =
- List.map (fun (id,a) -> (string_of_id id,a)) alist in
let rec subst = function
- Nvar(l,s) as x -> (try List.assoc s alist' with Not_found -> x)
+ Nvar(l,s) as x -> (try List.assoc s alist with Not_found -> x)
| Node(l,s,args) -> Node(l,s,List.map subst args)
- | Slam(l,so,a) -> Slam(l,so,subst a) (* TODO:enlever so de alist' ? *)
+ | Slam(l,so,a) -> Slam(l,so,subst a) (* TODO:enlever so de alist ? *)
| x -> x
in
subst ast
@@ -146,7 +142,8 @@ let real_subst_in_constr = replace_vars
(* Coq constants *)
-let coq_constant d s = make_path ("Coq" :: d) (id_of_string s) CCI
+let coq_constant d s =
+ make_path (List.map id_of_string ("Coq" :: d)) (id_of_string s) CCI
let bool_sp = coq_constant ["Init"; "Datatypes"] "bool"
let coq_true = mkMutConstruct (((bool_sp,0),1), [||])
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 5e0f9ad42..fc09cfa69 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -561,7 +561,7 @@ open Vernac
GEXTEND Gram
Pcoq.Vernac_.vernac:
[ [ IDENT "Global"; "Variable";
- l = LIST1 IDENT SEP ","; ":"; t = type_v; "." ->
+ l = LIST1 ident SEP ","; ":"; t = type_v; "." ->
let idl = List.map Ast.nvar l in
let d = Ast.dynamic (in_typev t) in
<:ast< (PROGVARIABLE (VERNACARGLIST ($LIST $idl)) (VERNACDYN $d)) >>
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index da3d464bb..ba4c4a616 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -215,6 +215,7 @@ let _ =
those having an ML extraction. *)
let extract_module m =
+ let m = Nametab.locate_loaded_library (Nametab.make_qualid [] m) in
let seg = Library.module_segment (Some m) in
let get_reference = function
| sp, Leaf o ->
@@ -242,10 +243,10 @@ let _ =
(function
| [VARG_STRING lang; VARG_VARGLIST o; VARG_IDENTIFIER m] ->
(fun () ->
- let m = Names.string_of_id m in
- Ocaml.current_module := m;
- let f = (String.uncapitalize m) ^ (file_suffix lang) in
- let prm = interp_options lang [] true m o in
+ Ocaml.current_module := Some m;
+ let ms = Names.string_of_id m in
+ let f = (String.uncapitalize ms) ^ (file_suffix lang) in
+ let prm = interp_options lang [] true ms o in
let rl = extract_module m in
let decls = optimize prm (decl_of_refs rl) in
let decls = List.filter (decl_mem rl) decls in
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 827381d1c..98ea283c7 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -385,7 +385,8 @@ module ModularParams = struct
in
let m = list_last (dirpath sp) in
id_of_string
- (if m = !current_module then s else (String.capitalize m) ^ "." ^ s)
+ (if Some m = !current_module then s
+ else (String.capitalize (string_of_id m)) ^ "." ^ s)
let rename_type_global r =
let id = Environ.id_of_global (Global.env()) r in
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 750afc782..960edb58a 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -395,7 +395,7 @@ module MonoPp = Make(MonoParams)
(*s Renaming issues in a modular extraction. *)
-let current_module = ref ""
+let current_module = ref None
module ModularParams = struct
@@ -424,7 +424,8 @@ module ModularParams = struct
in
let m = list_last (dirpath sp) in
id_of_string
- (if m = !current_module then s else (String.capitalize m) ^ "." ^ s)
+ (if Some m = !current_module then s
+ else (String.capitalize (string_of_id m)) ^ "." ^ s)
let rename_type_global r =
let id = Environ.id_of_global (Global.env()) r in
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 057d909fa..6ab76aded 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -22,7 +22,7 @@ val collect_lambda : ml_ast -> identifier list * ml_ast
val push_vars : identifier list -> identifier list * Idset.t ->
identifier list * (identifier list * Idset.t)
-val current_module : string ref
+val current_module : identifier option ref
(*s Production of Ocaml syntax. We export both a functor to be used for
extraction in the Coq toplevel and a function to extract some
@@ -32,7 +32,7 @@ open Mlutil
module Make : functor(P : Mlpp_param) -> Mlpp
-val current_module : string ref
+val current_module : Names.identifier option ref
val extract_to_file : string -> extraction_params -> ml_decl list -> unit
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 19b8534d1..926ca7951 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -23,7 +23,7 @@ let constr_of com = Astterm.interp_constr Evd.empty (Global.env()) com
(* Construction of constants *)
let constant dir s =
- let dir = "Coq"::"field"::dir in
+ let dir = make_dirpath (List.map id_of_string ("Coq"::"field"::dir)) in
let id = id_of_string s in
try
Declare.global_reference_in_absolute_module dir id
@@ -115,7 +115,7 @@ let field g =
| [|-(eq ?1 ? ?)] -> ?1
| [|-(eqT ?1 ? ?)] -> ?1>>) in
let th = VArg (Constr (lookup typ)) in
- (tac_interp [("FT",th)] [] (get_debug ()) <:tactic<Field_Gen FT>>) g
+ (tac_interp [(id_of_string "FT",th)] [] (get_debug ()) <:tactic<Field_Gen FT>>) g
(* Declaration of Field *)
let _ = hide_tactic "Field" (function _ -> field)
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 7307075be..7bf6441f7 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -220,7 +220,7 @@ let recognize_number t =
This is the right way to access to Coq constants in tactics ML code *)
let constant dir s =
- let dir = "Coq"::dir in
+ let dir = make_dirpath (List.map id_of_string ("Coq"::dir)) in
let id = id_of_string s in
try
Declare.global_reference_in_absolute_module dir id
@@ -384,7 +384,7 @@ let coq_imp_simp = lazy (logic_constant ["Decidable"] "imp_simp")
(* Section paths for unfold *)
open Closure
let make_coq_path dir s =
- let dir = "Coq"::dir in
+ let dir = make_dirpath (List.map id_of_string ("Coq"::dir)) in
let id = id_of_string s in
let ref =
try Nametab.locate_in_absolute_module dir id
diff --git a/contrib/ring/Setoid_ring_normalize.v b/contrib/ring/Setoid_ring_normalize.v
index 04e2aa16a..e49be3272 100644
--- a/contrib/ring/Setoid_ring_normalize.v
+++ b/contrib/ring/Setoid_ring_normalize.v
@@ -456,6 +456,8 @@ Proof.
NewDestruct l;Trivial.
Save.
+(* Hints Resolve ivl_aux_ok ics_aux_ok interp_m_ok. *)
+
Lemma canonical_sum_merge_ok : (x,y:canonical_sum)
(Aequiv (interp_cs (canonical_sum_merge x y))
(Aplus (interp_cs x) (interp_cs y))).
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index 7908af7ec..10ca06b78 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -120,7 +120,7 @@ open Proof_type
the constants are loaded in the environment *)
let constant dir s =
- let dir = "Coq"::"ring"::dir in
+ let dir = make_dirpath (List.map id_of_string ("Coq"::"ring"::dir)) in
let id = id_of_string s in
try
Declare.global_reference_in_absolute_module dir id
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index fad760cba..720c5a862 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -34,7 +34,7 @@ let mt_evd = Evd.empty
let constr_of com = Astterm.interp_constr mt_evd (Global.env()) com
let constant dir s =
- let dir = "Coq"::dir in
+ let dir = make_dirpath (List.map id_of_string ("Coq"::dir)) in
let id = id_of_string s in
try
Declare.global_reference_in_absolute_module dir id
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 95a93cde7..6e7548596 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -100,7 +100,8 @@ let could_have_namesakes o sp = (* namesake = omonimo in italian *)
let uri_of_path sp tag =
let module N = Names in
let ext_of_sp sp = ext_of_tag tag in
- "cic:/" ^ (String.concat "/" (N.wd_of_sp sp)) ^ "." ^ (ext_of_sp sp)
+ let dir = List.map N.string_of_id (N.wd_of_sp sp) in
+ "cic:/" ^ (String.concat "/" dir) ^ "." ^ (ext_of_sp sp)
;;
let string_of_sort =
@@ -795,8 +796,8 @@ let mkfilename dn sp ext =
match dn with
None -> None
| Some basedir ->
- Some (basedir ^ join_dirs basedir (N.wd_of_sp sp) ^
- "." ^ ext)
+ let dir = List.map N.string_of_id (N.wd_of_sp sp) in
+ Some (basedir ^ join_dirs basedir dir ^ "." ^ ext)
;;
(* print_object leaf_object id section_path directory_name formal_vars *)
@@ -914,9 +915,10 @@ and print_node n id sp bprintleaf dn =
print_if_verbose ("Suppongo gia' stampato " ^ Names.string_of_id id ^ "\n")
end
end
- | L.OpenedSection (s,_) -> print_if_verbose ("OpenDir " ^ s ^ "\n")
- | L.ClosedSection (_,s,state) ->
- print_if_verbose("ClosedDir " ^ s ^ "\n") ;
+ | L.OpenedSection (id,_) ->
+ print_if_verbose ("OpenDir " ^ Names.string_of_id id ^ "\n")
+ | L.ClosedSection (_,id,state) ->
+ print_if_verbose("ClosedDir " ^ Names.string_of_id id ^ "\n") ;
if bprintleaf then
begin
(* open a new scope *)
@@ -963,12 +965,12 @@ let printModule id dn =
let module X = Xml in
let str = N.string_of_id id in
let sp = Lib.make_path id N.OBJ in
- let ls = L.module_segment (Some str) in
+ let ls = L.module_segment (Some [id]) in
print_if_verbose ("MODULE_BEGIN " ^ str ^ " " ^ N.string_of_path sp ^ " " ^
- (snd (L.module_filename str)) ^ "\n") ;
+ (L.module_full_filename [id]) ^ "\n") ;
print_closed_section str (List.rev ls) dn ;
print_if_verbose ("MODULE_END " ^ str ^ " " ^ N.string_of_path sp ^ " " ^
- (snd (L.module_filename str)) ^ "\n")
+ (L.module_full_filename [id]) ^ "\n")
;;
(* printSection identifier directory_name *)
@@ -982,18 +984,18 @@ let printSection id dn =
let module L = Library in
let module N = Names in
let module X = Xml in
- let str = N.string_of_id id in
let sp = Lib.make_path id N.OBJ in
let ls =
let rec find_closed_section =
function
[] -> raise Not_found
- | (_,Lib.ClosedSection (_,str',ls))::_ when str' = str -> ls
+ | (_,Lib.ClosedSection (_,id',ls))::_ when id' = id -> ls
| _::t -> find_closed_section t
in
print_string ("Searching " ^ Names.string_of_path sp ^ "\n") ;
find_closed_section (Lib.contents_after None)
in
+ let str = N.string_of_id id in
print_if_verbose ("SECTION_BEGIN " ^ str ^ " " ^ N.string_of_path sp ^ "\n");
print_closed_section str ls dn ;
print_if_verbose ("SECTION_END " ^ str ^ " " ^ N.string_of_path sp ^ "\n")
generated by cgit v1.2.3 (git 2.39.1) at 2025-02-08 00:29:11 +0000