From 67f5c70a480c95cfb819fc68439781b5e5e95794 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 14 Dec 2012 15:56:25 +0000 Subject: Modulification of identifier git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/romega/const_omega.ml | 10 +++++----- plugins/romega/g_romega.ml4 | 2 +- plugins/romega/refl_omega.ml | 8 ++++---- 3 files changed, 10 insertions(+), 10 deletions(-) (limited to 'plugins/romega') diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 5b57a0d17..92135d497 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -22,10 +22,10 @@ let string_of_global r = let prefix = match Names.repr_dirpath dp with | [] -> "" | m::_ -> - let s = Names.string_of_id m in + let s = Names.Id.to_string m in if List.mem s meaningful_submodule then s^"." else "" in - prefix^(Names.string_of_id (Nametab.basename_of_global r)) + prefix^(Names.Id.to_string (Nametab.basename_of_global r)) let destructurate t = let c, args = Term.decompose_app t in @@ -36,7 +36,7 @@ let destructurate t = Kapp (string_of_global (Globnames.ConstructRef csp), args) | Term.Ind isp, args -> Kapp (string_of_global (Globnames.IndRef isp), args) - | Term.Var id,[] -> Kvar(Names.string_of_id id) + | Term.Var id,[] -> Kvar(Names.Id.to_string id) | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body) | Term.Prod (Names.Name _,_,_),[] -> Errors.error "Omega: Not a quantifier-free goal" @@ -296,13 +296,13 @@ let coq_Zneg = lazy (bin_constant "Zneg") let recognize t = let rec loop t = let f,l = dest_const_apply t in - match Names.string_of_id f,l with + match Names.Id.to_string f,l with "xI",[t] -> Bigint.add Bigint.one (Bigint.mult Bigint.two (loop t)) | "xO",[t] -> Bigint.mult Bigint.two (loop t) | "xH",[] -> Bigint.one | _ -> failwith "not a number" in let f,l = dest_const_apply t in - match Names.string_of_id f,l with + match Names.Id.to_string f,l with "Zpos",[t] -> loop t | "Zneg",[t] -> Bigint.neg (loop t) | "Z0",[] -> Bigint.zero diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 5a843e2b7..a68196e8c 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -37,6 +37,6 @@ END TACTIC EXTEND romega' | [ "romega" "with" ne_ident_list(l) ] -> - [ romega_tactic (List.map Names.string_of_id l) ] + [ romega_tactic (List.map Names.Id.to_string l) ] | [ "romega" "with" "*" ] -> [ romega_tactic ["nat";"positive";"N";"Z"] ] END diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index e573f2006..e3674fae0 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -40,7 +40,7 @@ type occ_path = occ_step list (* chemin identifiant une proposition sous forme du nom de l'hypothèse et d'une liste de pas à partir de la racine de l'hypothèse *) -type occurence = {o_hyp : Names.identifier; o_path : occ_path} +type occurence = {o_hyp : Names.Id.t; o_path : occ_path} (* \subsection{refiable formulas} *) type oformula = @@ -137,7 +137,7 @@ type context_content = (* \section{Specific utility functions to handle base types} *) (* Nom arbitraire de l'hypothèse codant la négation du but final *) -let id_concl = Names.id_of_string "__goal__" +let id_concl = Names.Id.of_string "__goal__" (* Initialisation de l'environnement de réification de la tactique *) let new_environment () = { @@ -746,7 +746,7 @@ let reify_gl env gl = (i,t) :: lhyps -> let t' = oproposition_of_constr env (false,[],i,[]) gl t in if !debug then begin - Printf.printf " %s: " (Names.string_of_id i); + Printf.printf " %s: " (Names.Id.to_string i); pprint stdout t'; Printf.printf "\n" end; @@ -840,7 +840,7 @@ let display_systems syst_list = (List.map (function O_left -> "L" | O_right -> "R" | O_mono -> "M") oformula_eq.e_origin.o_path)); Printf.printf "\n Origin: %s (negated : %s)\n\n" - (Names.string_of_id oformula_eq.e_origin.o_hyp) + (Names.Id.to_string oformula_eq.e_origin.o_hyp) (if oformula_eq.e_negated then "yes" else "no") in let display_system syst = -- cgit v1.2.3