From 6b45f2d36929162cf92272bb60c2c245d9a0ead3 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 22 Jun 2012 15:14:30 +0000 Subject: Added an indirection with respect to Loc in Compat. As many [open Compat] were closed (i.e. the only remaining ones are those of printing/parsing). Meanwhile, a simplified interface is provided in loc.mli. This also permits to put Pp in Clib, because it does not depend on CAMLP4/5 anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/decl_mode/decl_expr.mli | 4 +-- plugins/decl_mode/decl_interp.ml | 39 +++++++++++++-------------- plugins/decl_mode/decl_proof_instr.ml | 4 +-- plugins/firstorder/g_ground.ml4 | 2 +- plugins/firstorder/instances.ml | 2 +- plugins/funind/g_indfun.ml4 | 8 +++--- plugins/funind/glob_term_to_relation.ml | 48 ++++++++++++++++----------------- plugins/funind/glob_termops.ml | 22 +++++++-------- plugins/funind/glob_termops.mli | 6 ++--- plugins/funind/indfun.ml | 36 ++++++++++++------------- plugins/funind/indfun.mli | 2 +- plugins/funind/indfun_common.ml | 2 +- plugins/funind/invfun.ml | 14 +++++----- plugins/funind/merge.ml | 28 +++++++++---------- plugins/funind/recdef.ml | 14 +++++----- plugins/quote/g_quote.ml4 | 4 +-- plugins/setoid_ring/newring.ml4 | 42 ++++++++++++++--------------- plugins/syntax/ascii_syntax.ml | 2 +- plugins/syntax/nat_syntax.ml | 2 +- plugins/syntax/numbers_syntax.ml | 10 +++---- plugins/syntax/r_syntax.ml | 6 ++--- plugins/syntax/string_syntax.ml | 4 +-- plugins/syntax/z_syntax.ml | 16 +++++------ 23 files changed, 158 insertions(+), 159 deletions(-) (limited to 'plugins') diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli index 78ffda215..d0fdfa0f3 100644 --- a/plugins/decl_mode/decl_expr.mli +++ b/plugins/decl_mode/decl_expr.mli @@ -77,13 +77,13 @@ type ('hyp,'constr,'pat,'tac) gen_proof_instr= type raw_proof_instr = - ((identifier*(Constrexpr.constr_expr option)) located, + ((identifier*(Constrexpr.constr_expr option)) Loc.located, Constrexpr.constr_expr, Constrexpr.cases_pattern_expr, raw_tactic_expr) gen_proof_instr type glob_proof_instr = - ((identifier*(Genarg.glob_constr_and_expr option)) located, + ((identifier*(Genarg.glob_constr_and_expr option)) Loc.located, Genarg.glob_constr_and_expr, Constrexpr.cases_pattern_expr, Tacexpr.glob_tactic_expr) gen_proof_instr diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index a067440cb..da3f9619b 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -18,7 +18,6 @@ open Pretyping open Glob_term open Term open Pp -open Compat open Decl_kinds open Misctypes @@ -188,16 +187,16 @@ let interp_constr_or_thesis check_sort sigma env = function let abstract_one_hyp inject h glob = match h with Hvar (loc,(id,None)) -> - GProd (dummy_loc,Name id, Explicit, GHole (loc,Evar_kinds.BinderType (Name id)), glob) + GProd (Loc.ghost,Name id, Explicit, GHole (loc,Evar_kinds.BinderType (Name id)), glob) | Hvar (loc,(id,Some typ)) -> - GProd (dummy_loc,Name id, Explicit, fst typ, glob) + GProd (Loc.ghost,Name id, Explicit, fst typ, glob) | Hprop st -> - GProd (dummy_loc,st.st_label, Explicit, inject st.st_it, glob) + GProd (Loc.ghost,st.st_label, Explicit, inject st.st_it, glob) let glob_constr_of_hyps inject hyps head = List.fold_right (abstract_one_hyp inject) hyps head -let glob_prop = GSort (dummy_loc,GProp) +let glob_prop = GSort (Loc.ghost,GProp) let rec match_hyps blend names constr = function [] -> [],substl names constr @@ -245,27 +244,27 @@ let rec glob_of_pat = let mind= fst (Global.lookup_inductive ind) in let rec add_params n q = if n<=0 then q else - add_params (pred n) (GHole(dummy_loc, + add_params (pred n) (GHole(Loc.ghost, Evar_kinds.TomatchTypeParameter(ind,n))::q) in let args = List.map glob_of_pat lpat in - glob_app(loc,GRef(dummy_loc,Globnames.ConstructRef cstr), + glob_app(loc,GRef(Loc.ghost,Globnames.ConstructRef cstr), add_params mind.Declarations.mind_nparams args) let prod_one_hyp = function (loc,(id,None)) -> (fun glob -> - GProd (dummy_loc,Name id, Explicit, + GProd (Loc.ghost,Name id, Explicit, GHole (loc,Evar_kinds.BinderType (Name id)), glob)) | (loc,(id,Some typ)) -> (fun glob -> - GProd (dummy_loc,Name id, Explicit, fst typ, glob)) + GProd (Loc.ghost,Name id, Explicit, fst typ, glob)) let prod_one_id (loc,id) glob = - GProd (dummy_loc,Name id, Explicit, + GProd (Loc.ghost,Name id, Explicit, GHole (loc,Evar_kinds.BinderType (Name id)), glob) let let_in_one_alias (id,pat) glob = - GLetIn (dummy_loc,Name id, glob_of_pat pat, glob) + GLetIn (Loc.ghost,Name id, glob_of_pat pat, glob) let rec bind_primary_aliases map pat = match pat with @@ -335,7 +334,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = (if expected = 0 then str "none" else int expected) ++ spc () ++ str "expected.") in let app_ind = - let rind = GRef (dummy_loc,Globnames.IndRef pinfo.per_ind) in + let rind = GRef (Loc.ghost,Globnames.IndRef pinfo.per_ind) in let rparams = List.map detype_ground pinfo.per_params in let rparams_rec = List.map @@ -343,18 +342,18 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = GVar (loc,id)) params in let dum_args= list_tabulate - (fun _ -> GHole (dummy_loc,Evar_kinds.QuestionMark (Evar_kinds.Define false))) + (fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false))) oib.Declarations.mind_nrealargs in - glob_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in + glob_app(Loc.ghost,rind,rparams@rparams_rec@dum_args) in let pat_vars,aliases,patt = interp_pattern env pat in let inject = function - Thesis (Plain) -> Glob_term.GSort(dummy_loc,GProp) + Thesis (Plain) -> Glob_term.GSort(Loc.ghost,GProp) | Thesis (For rec_occ) -> if not (List.mem rec_occ pat_vars) then errorlabstrm "suppose it is" (str "Variable " ++ Nameops.pr_id rec_occ ++ str " does not occur in pattern."); - Glob_term.GSort(dummy_loc,GProp) + Glob_term.GSort(Loc.ghost,GProp) | This (c,_) -> c in let term1 = glob_constr_of_hyps inject hyps glob_prop in let loc_ids,npatt = @@ -362,8 +361,8 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = let npatt= deanonymize rids patt in List.rev (fst !rids),npatt in let term2 = - GLetIn(dummy_loc,Anonymous, - GCast(dummy_loc,glob_of_pat npatt, + GLetIn(Loc.ghost,Anonymous, + GCast(Loc.ghost,glob_of_pat npatt, CastConv app_ind),term1) in let term3=List.fold_right let_in_one_alias aliases term2 in let term4=List.fold_right prod_one_id loc_ids term3 in @@ -418,11 +417,11 @@ let interp_casee sigma env = function let abstract_one_arg = function (loc,(id,None)) -> (fun glob -> - GLambda (dummy_loc,Name id, Explicit, + GLambda (Loc.ghost,Name id, Explicit, GHole (loc,Evar_kinds.BinderType (Name id)), glob)) | (loc,(id,Some typ)) -> (fun glob -> - GLambda (dummy_loc,Name id, Explicit, fst typ, glob)) + GLambda (Loc.ghost,Name id, Explicit, fst typ, glob)) let glob_constr_of_fun args body = List.fold_right abstract_one_arg args (fst body) diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 2d069b497..b59ab5c0f 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -751,7 +751,7 @@ let consider_tac c hyps gls = | _ -> let id = pf_get_new_id (id_of_string "_tmp") gls in tclTHEN - (forward None (Some (dummy_loc, IntroIdentifier id)) c) + (forward None (Some (Loc.ghost, IntroIdentifier id)) c) (consider_match false [] [id] hyps) gls @@ -1290,7 +1290,7 @@ let understand_my_constr c gls = let nc = names_of_rel_context env in let rawc = Detyping.detype false [] nc c in let rec frob = function - | GEvar _ -> GHole (dummy_loc,Evar_kinds.QuestionMark Evar_kinds.Expand) + | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand) | rc -> map_glob_constr frob rc in Pretyping.understand_tcc (sig_sig gls) env ~expected_type:(pf_concl gls) (frob rawc) diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index b009107dc..3f0c704ad 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -107,7 +107,7 @@ open Genarg open Ppconstr open Printer let pr_firstorder_using_raw _ _ _ = prlist_with_sep pr_comma pr_reference -let pr_firstorder_using_glob _ _ _ = prlist_with_sep pr_comma (pr_or_var (pr_located pr_global)) +let pr_firstorder_using_glob _ _ _ = prlist_with_sep pr_comma (pr_or_var (Loc.pr_located pr_global)) let pr_firstorder_using_typed _ _ _ = prlist_with_sep pr_comma pr_global ARGUMENT EXTEND firstorder_using diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index bc15cb501..195e6afa3 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -128,7 +128,7 @@ let mk_open_instance id gl m t= match t with GLambda(loc,name,k,_,t0)-> let t1=raux (n-1) t0 in - GLambda(loc,name,k,GHole (dummy_loc,Evar_kinds.BinderType name),t1) + GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name),t1) | _-> anomaly "can't happen" in let ntt=try Pretyping.understand evmap env (raux m rawt) diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 169f4d120..9fcfeb36c 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -139,7 +139,7 @@ module FunctionGram = struct let gec s = Gram.entry_create ("Function."^s) (* types *) - let function_rec_definition_loc : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) located Gram.entry = gec "function_rec_definition_loc" + let function_rec_definition_loc : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located Gram.entry = gec "function_rec_definition_loc" end open FunctionGram @@ -151,7 +151,7 @@ GEXTEND Gram ; END -type 'a function_rec_definition_loc_argtype = ((Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) located, 'a) Genarg.abstract_argument_type +type 'a function_rec_definition_loc_argtype = ((Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located, 'a) Genarg.abstract_argument_type let (wit_function_rec_definition_loc : Genarg.tlevel function_rec_definition_loc_argtype), (globwit_function_rec_definition_loc : Genarg.glevel function_rec_definition_loc_argtype), @@ -460,9 +460,9 @@ VERNAC COMMAND EXTEND MergeFunind "with" "(" ident(id2) ne_ident_list(cl2) ")" "using" ident(id) ] -> [ let f1 = Constrintern.interp_constr Evd.empty (Global.env()) - (CRef (Libnames.Ident (Pp.dummy_loc,id1))) in + (CRef (Libnames.Ident (Loc.ghost,id1))) in let f2 = Constrintern.interp_constr Evd.empty (Global.env()) - (CRef (Libnames.Ident (Pp.dummy_loc,id2))) in + (CRef (Libnames.Ident (Loc.ghost,id2))) in let f1type = Typing.type_of (Global.env()) Evd.empty f1 in let f2type = Typing.type_of (Global.env()) Evd.empty f2 in let ar1 = List.length (fst (decompose_prod f1type)) in diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 7b341e581..93e1d105e 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -273,8 +273,8 @@ let make_discr_match_brl i = list_map_i (fun j (_,idl,patl,_) -> if j=i - then (dummy_loc,idl,patl, mkGRef (Lazy.force coq_True_ref)) - else (dummy_loc,idl,patl, mkGRef (Lazy.force coq_False_ref)) + then (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_True_ref)) + else (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_False_ref)) ) 0 (* @@ -511,9 +511,9 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = | u::l -> match t with | GLambda(loc,na,_,nat,b) -> - GLetIn(dummy_loc,na,u,aux b l) + GLetIn(Loc.ghost,na,u,aux b l) | _ -> - GApp(dummy_loc,t,l) + GApp(Loc.ghost,t,l) in build_entry_lc env funnames avoid (aux f args) | GVar(_,id) when Idset.mem id funnames -> @@ -571,7 +571,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let new_b = replace_var_by_term id - (GVar(dummy_loc,id)) + (GVar(Loc.ghost,id)) b in (Name new_id,new_b,new_avoid) @@ -661,7 +661,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = assert (Array.length case_pats = 2); let brl = list_map_i - (fun i x -> (dummy_loc,[],[case_pats.(i)],x)) + (fun i x -> (Loc.ghost,[],[case_pats.(i)],x)) 0 [lhs;rhs] in @@ -692,7 +692,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let case_pats = build_constructors_of_type ind nal_as_glob_constr in assert (Array.length case_pats = 1); let br = - (dummy_loc,[],[case_pats.(0)],e) + (Loc.ghost,[],[case_pats.(0)],e) in let match_expr = mkGCases(None,[b,(Anonymous,None)],[br]) in build_entry_lc env funnames avoid match_expr @@ -981,8 +981,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = ((Util.list_chop nparam args')) in let rt_typ = - GApp(Pp.dummy_loc, - GRef (Pp.dummy_loc,Globnames.IndRef ind), + GApp(Loc.ghost, + GRef (Loc.ghost,Globnames.IndRef ind), (List.map (fun p -> Detyping.detype false [] (Termops.names_of_rel_context env) @@ -1130,7 +1130,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = then new_b, Idset.remove id (Idset.filter not_free_in_t id_to_exclude) else - GProd(dummy_loc,n,k,t,new_b),Idset.filter not_free_in_t id_to_exclude + GProd(Loc.ghost,n,k,t,new_b),Idset.filter not_free_in_t id_to_exclude | _ -> anomaly "Should not have an anonymous function here" (* We have renamed all the anonymous functions during alpha_renaming phase *) @@ -1149,7 +1149,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = match n with | Name id when Idset.mem id id_to_exclude && depth >= nb_args -> new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude) - | _ -> GLetIn(dummy_loc,n,t,new_b), + | _ -> GLetIn(Loc.ghost,n,t,new_b), Idset.filter not_free_in_t id_to_exclude end | GLetTuple(_,nal,(na,rto),t,b) -> @@ -1175,7 +1175,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (* | Name id when Idset.mem id id_to_exclude -> *) (* new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude) *) (* | _ -> *) - GLetTuple(dummy_loc,nal,(na,None),t,new_b), + GLetTuple(Loc.ghost,nal,(na,None),t,new_b), Idset.filter not_free_in_t (Idset.union id_to_exclude id_to_exclude') end @@ -1261,9 +1261,9 @@ let rec rebuild_return_type rt = Constrexpr.CProdN(loc,n,rebuild_return_type t') | Constrexpr.CLetIn(loc,na,t,t') -> Constrexpr.CLetIn(loc,na,t,rebuild_return_type t') - | _ -> Constrexpr.CProdN(dummy_loc,[[dummy_loc,Names.Anonymous], + | _ -> Constrexpr.CProdN(Loc.ghost,[[Loc.ghost,Names.Anonymous], Constrexpr.Default Decl_kinds.Explicit,rt], - Constrexpr.CSort(dummy_loc,GType None)) + Constrexpr.CSort(Loc.ghost,GType None)) let do_build_inductive @@ -1303,12 +1303,12 @@ let do_build_inductive (fun (n,t,is_defined) acc -> if is_defined then - Constrexpr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t, + Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Idset.empty t, acc) else Constrexpr.CProdN - (dummy_loc, - [[(dummy_loc,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t], + (Loc.ghost, + [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t], acc ) ) @@ -1369,12 +1369,12 @@ let do_build_inductive (fun (n,t,is_defined) acc -> if is_defined then - Constrexpr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t, + Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Idset.empty t, acc) else Constrexpr.CProdN - (dummy_loc, - [[(dummy_loc,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t], + (Loc.ghost, + [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t], acc ) ) @@ -1391,17 +1391,17 @@ let do_build_inductive (fun (n,t,is_defined) -> if is_defined then - Constrexpr.LocalRawDef((dummy_loc,n), Constrextern.extern_glob_constr Idset.empty t) + Constrexpr.LocalRawDef((Loc.ghost,n), Constrextern.extern_glob_constr Idset.empty t) else Constrexpr.LocalRawAssum - ([(dummy_loc,n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Idset.empty t) + ([(Loc.ghost,n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Idset.empty t) ) rels_params in let ext_rels_constructors = Array.map (List.map (fun (id,t) -> - false,((dummy_loc,id), + false,((Loc.ghost,id), Flags.with_option Flags.raw_print (Constrextern.extern_glob_type Idset.empty) ((* zeta_normalize *) t) @@ -1410,7 +1410,7 @@ let do_build_inductive (rel_constructors) in let rel_ind i ext_rel_constructors = - ((dummy_loc,relnames.(i)), + ((Loc.ghost,relnames.(i)), rel_params, Some rel_arities.(i), ext_rel_constructors),[] diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 8967a3ec8..f678b898b 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -11,18 +11,18 @@ let idmap_is_empty m = m = Idmap.empty (* Some basic functions to rebuild glob_constr - In each of them the location is Util.dummy_loc + In each of them the location is Loc.ghost *) -let mkGRef ref = GRef(dummy_loc,ref) -let mkGVar id = GVar(dummy_loc,id) -let mkGApp(rt,rtl) = GApp(dummy_loc,rt,rtl) -let mkGLambda(n,t,b) = GLambda(dummy_loc,n,Explicit,t,b) -let mkGProd(n,t,b) = GProd(dummy_loc,n,Explicit,t,b) -let mkGLetIn(n,t,b) = GLetIn(dummy_loc,n,t,b) -let mkGCases(rto,l,brl) = GCases(dummy_loc,Term.RegularStyle,rto,l,brl) -let mkGSort s = GSort(dummy_loc,s) -let mkGHole () = GHole(dummy_loc,Evar_kinds.BinderType Anonymous) -let mkGCast(b,t) = GCast(dummy_loc,b,CastConv t) +let mkGRef ref = GRef(Loc.ghost,ref) +let mkGVar id = GVar(Loc.ghost,id) +let mkGApp(rt,rtl) = GApp(Loc.ghost,rt,rtl) +let mkGLambda(n,t,b) = GLambda(Loc.ghost,n,Explicit,t,b) +let mkGProd(n,t,b) = GProd(Loc.ghost,n,Explicit,t,b) +let mkGLetIn(n,t,b) = GLetIn(Loc.ghost,n,t,b) +let mkGCases(rto,l,brl) = GCases(Loc.ghost,Term.RegularStyle,rto,l,brl) +let mkGSort s = GSort(Loc.ghost,s) +let mkGHole () = GHole(Loc.ghost,Evar_kinds.BinderType Anonymous) +let mkGCast(b,t) = GCast(Loc.ghost,b,CastConv t) (* Some basic functions to decompose glob_constrs diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 437ba225d..9cf83df15 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -15,7 +15,7 @@ val pattern_to_term : cases_pattern -> glob_constr (* Some basic functions to rebuild glob_constr - In each of them the location is Util.dummy_loc + In each of them the location is Util.Loc.ghost *) val mkGRef : Globnames.global_reference -> glob_constr val mkGVar : Names.identifier -> glob_constr @@ -85,9 +85,9 @@ val alpha_rt : Names.identifier list -> glob_constr -> glob_constr (* same as alpha_rt but for case branches *) val alpha_br : Names.identifier list -> - Pp.loc * Names.identifier list * Glob_term.cases_pattern list * + Loc.t * Names.identifier list * Glob_term.cases_pattern list * Glob_term.glob_constr -> - Pp.loc * Names.identifier list * Glob_term.cases_pattern list * + Loc.t * Names.identifier list * Glob_term.cases_pattern list * Glob_term.glob_constr diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 2a6a7dea3..5b9bf44c3 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -182,7 +182,7 @@ let build_newrecursive l = match body_opt with | Some body -> (fixna,bll,ar,body) - | None -> user_err_loc (dummy_loc,"Function",str "Body of Function must be given") + | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") ) l in build_newrecursive l' @@ -321,7 +321,7 @@ let generate_principle on_error (*i The next call to mk_rel_id is valid since we have just construct the graph Ensures by : do_built i*) - let f_R_mut = Ident (dummy_loc,mk_rel_id (List.nth names 0)) in + let f_R_mut = Ident (Loc.ghost,mk_rel_id (List.nth names 0)) in let ind_kn = fst (locate_with_msg (pr_reference f_R_mut++str ": Not an inductive type!") @@ -363,7 +363,7 @@ let generate_principle on_error let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = match fixpoint_exprl with | [((_,fname),_,bl,ret_type,body),_] when not is_rec -> - let body = match body with | Some body -> body | None -> user_err_loc (dummy_loc,"Function",str "Body of Function must be given") in + let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in Command.do_definition fname (Decl_kinds.Global,Decl_kinds.Definition) bl None body (Some ret_type) (fun _ _ -> ()) | _ -> @@ -397,8 +397,8 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas let unbounded_eq = let f_app_args = Constrexpr.CAppExpl - (dummy_loc, - (None,(Ident (dummy_loc,fname))) , + (Loc.ghost, + (None,(Ident (Loc.ghost,fname))) , (List.map (function | _,Anonymous -> assert false @@ -408,7 +408,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas ) ) in - Constrexpr.CApp (dummy_loc,(None,Constrexpr_ops.mkRefC (Qualid (dummy_loc,(qualid_of_string "Logic.eq")))), + Constrexpr.CApp (Loc.ghost,(None,Constrexpr_ops.mkRefC (Qualid (Loc.ghost,(qualid_of_string "Logic.eq")))), [(f_app_args,None);(body,None)]) in let eq = Constrexpr_ops.prod_constr_expr unbounded_eq args in @@ -465,13 +465,13 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas | None -> let ltof = let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) in - Libnames.Qualid (dummy_loc,Libnames.qualid_of_path + Libnames.Qualid (Loc.ghost,Libnames.qualid_of_path (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (id_of_string "ltof"))) in let fun_from_mes = let applied_mes = Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg]) in - Constrexpr_ops.mkLambdaC ([(dummy_loc,Name wf_arg)],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes) + Constrexpr_ops.mkLambdaC ([(Loc.ghost,Name wf_arg)],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes) in let wf_rel_from_mes = Constrexpr_ops.mkAppC(Constrexpr_ops.mkRefC ltof,[wf_arg_type;fun_from_mes]) @@ -482,7 +482,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas let a = Names.id_of_string "___a" in let b = Names.id_of_string "___b" in Constrexpr_ops.mkLambdaC( - [dummy_loc,Name a;dummy_loc,Name b], + [Loc.ghost,Name a;Loc.ghost,Name b], Constrexpr.Default Explicit, wf_arg_type, Constrexpr_ops.mkAppC(wf_rel_expr, @@ -590,12 +590,12 @@ let rec rebuild_bl (aux,assoc) bl typ = (if new_nal' = [] && rest = [] then typ' else if new_nal' = [] - then CProdN(dummy_loc,rest,typ') - else CProdN(dummy_loc,((new_nal',bk',nal't)::rest),typ')) + then CProdN(Loc.ghost,rest,typ') + else CProdN(Loc.ghost,((new_nal',bk',nal't)::rest),typ')) else let captured_nal,non_captured_nal = list_chop lnal' nal in rebuild_nal ((LocalRawAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't)::aux), (make_assoc assoc nal' captured_nal)) - bk bl' non_captured_nal (lnal - lnal') (CProdN(dummy_loc,rest,typ')) + bk bl' non_captured_nal (lnal - lnal') (CProdN(Loc.ghost,rest,typ')) | _ -> assert false let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ @@ -628,7 +628,7 @@ let do_generate_principle on_error register_built interactive_proof | _ -> assert false in let fixpoint_exprl = [fixpoint_expr] in - let body = match body with | Some body -> body | None -> user_err_loc (dummy_loc,"Function",str "Body of Function must be given") in + let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let using_lemmas = [] in let pre_hook = @@ -652,7 +652,7 @@ let do_generate_principle on_error register_built interactive_proof let fixpoint_exprl = [fixpoint_expr] in let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let using_lemmas = [] in - let body = match body with | Some body -> body | None -> user_err_loc (dummy_loc,"Function",str "Body of Function must be given") in + let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in let pre_hook = generate_principle on_error @@ -701,7 +701,7 @@ let rec add_args id new_args b = | CRef r -> begin match r with | Libnames.Ident(loc,fname) when fname = id -> - CAppExpl(dummy_loc,(None,r),new_args) + CAppExpl(Loc.ghost,(None,r),new_args) | _ -> b end | CFix _ | CCoFix _ -> anomaly "add_args : todo" @@ -789,7 +789,7 @@ let rec chop_n_arrow n t = aux (n - nal_l) nal_ta' else let new_t' = - Constrexpr.CProdN(dummy_loc, + Constrexpr.CProdN(Loc.ghost, ((snd (list_chop n nal)),k,t'')::nal_ta',t') in raise (Stop new_t') @@ -867,14 +867,14 @@ let make_graph (f_ref:global_reference) = ) in let b' = add_args (snd id) new_args b in - (((id, ( Some (dummy_loc,rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) + (((id, ( Some (Loc.ghost,rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) ) fixexprl in l | _ -> let id = id_of_label (con_label c) in - [((dummy_loc,id),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]] + [((Loc.ghost,id),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]] in do_generate_principle error_error false false expr_list; (* We register the infos *) diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index bb3071782..56fc9bd2c 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -17,7 +17,7 @@ val functional_induction : bool -> Term.constr -> (Term.constr * Term.constr bindings) option -> - intro_pattern_expr Pp.located option -> + intro_pattern_expr Loc.located option -> Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 8443959b4..ff62a5c38 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -113,7 +113,7 @@ let list_add_set_eq eq_fun x l = let const_of_id id = let _,princ_ref = - qualid_of_reference (Libnames.Ident (Pp.dummy_loc,id)) + qualid_of_reference (Libnames.Ident (Loc.ghost,id)) in try Nametab.locate_constant princ_ref with Not_found -> Errors.error ("cannot find "^ string_of_id id) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 7745996c5..d8f999ec5 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -274,7 +274,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.map (fun (_,_,br_type) -> List.map - (fun id -> dummy_loc, IntroIdentifier id) + (fun id -> Loc.ghost, IntroIdentifier id) (generate_fresh_id (id_of_string "y") ids (List.length (fst (decompose_prod_assum br_type)))) ) branches @@ -459,7 +459,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.fold_left2 (fun (bindings,avoid) (x,_,_) p -> let id = Namegen.next_ident_away (Nameops.out_name x) avoid in - (*(dummy_loc,Glob_term.NamedHyp id,p)*)p::bindings,id::avoid + (*(Loc.ghost,Glob_term.NamedHyp id,p)*)p::bindings,id::avoid ) ([],pf_ids_of_hyps g) princ_infos.params @@ -469,7 +469,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.rev (fst (List.fold_left2 (fun (bindings,avoid) (x,_,_) p -> let id = Namegen.next_ident_away (Nameops.out_name x) avoid in - (*(dummy_loc,Glob_term.NamedHyp id,(nf_zeta p))*) (nf_zeta p)::bindings,id::avoid) + (*(Loc.ghost,Glob_term.NamedHyp id,(nf_zeta p))*) (nf_zeta p)::bindings,id::avoid) ([],avoid) princ_infos.predicates (lemmas))) @@ -538,13 +538,13 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.map (fun (_,_,br_type) -> List.map - (fun id -> dummy_loc, Genarg.IntroIdentifier id) + (fun id -> Loc.ghost, Genarg.IntroIdentifier id) (generate_fresh_id (id_of_string "y") ids (List.length (fst (decompose_prod_assum br_type)))) ) branches in (* before building the full intro pattern for the principle *) - let pat = Some (dummy_loc,Genarg.IntroOrAndPattern intro_pats) in + let pat = Some (Loc.ghost,Genarg.IntroOrAndPattern intro_pats) in let eq_ind = Coqlib.build_coq_eq () in let eq_construct = mkConstruct((destInd eq_ind),1) in (* The next to referencies will be used to find out which constructor to apply in each branch *) @@ -682,7 +682,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.fold_left2 (fun (bindings,avoid) (x,_,_) p -> let id = Namegen.next_ident_away (Nameops.out_name x) avoid in - (dummy_loc,Glob_term.NamedHyp id,p)::bindings,id::avoid + (Loc.ghost,Glob_term.NamedHyp id,p)::bindings,id::avoid ) ([],pf_ids_of_hyps g) princ_infos.params @@ -692,7 +692,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.rev (fst (List.fold_left2 (fun (bindings,avoid) (x,_,_) p -> let id = Namegen.next_ident_away (Nameops.out_name x) avoid in - (dummy_loc,Glob_term.NamedHyp id,(nf_zeta p))::bindings,id::avoid) + (Loc.ghost,Glob_term.NamedHyp id,(nf_zeta p))::bindings,id::avoid) ([],avoid) princ_infos.predicates (lemmas))) diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index af7506103..03aee3068 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -70,7 +70,7 @@ let isVarf f x = in global environment. *) let ident_global_exist id = try - let ans = CRef (Libnames.Ident (dummy_loc,id)) in + let ans = CRef (Libnames.Ident (Loc.ghost,id)) in let _ = ignore (Constrintern.intern_constr Evd.empty (Global.env()) ans) in true with _ -> false @@ -517,16 +517,16 @@ let rec merge_app c1 c2 id1 id2 shift filter_shift_stable = | GApp(_,f1, arr1), GApp(_,f2,arr2) when isVarf id1 f1 && isVarf id2 f2 -> let _ = prstr "\nICI1!\n";Pp.flush_all() in let args = filter_shift_stable lnk (arr1 @ arr2) in - GApp (dummy_loc,GVar (dummy_loc,shift.ident) , args) + GApp (Loc.ghost,GVar (Loc.ghost,shift.ident) , args) | GApp(_,f1, arr1), GApp(_,f2,arr2) -> raise NoMerge | GLetIn(_,nme,bdy,trm) , _ -> let _ = prstr "\nICI2!\n";Pp.flush_all() in let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in - GLetIn(dummy_loc,nme,bdy,newtrm) + GLetIn(Loc.ghost,nme,bdy,newtrm) | _, GLetIn(_,nme,bdy,trm) -> let _ = prstr "\nICI3!\n";Pp.flush_all() in let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in - GLetIn(dummy_loc,nme,bdy,newtrm) + GLetIn(Loc.ghost,nme,bdy,newtrm) | _ -> let _ = prstr "\nICI4!\n";Pp.flush_all() in raise NoMerge @@ -535,16 +535,16 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable = match c1 , c2 with | GApp(_,f1, arr1), GApp(_,f2,arr2) -> let args = filter_shift_stable lnk (arr1 @ arr2) in - GApp (dummy_loc,GVar(dummy_loc,shift.ident) , args) + GApp (Loc.ghost,GVar(Loc.ghost,shift.ident) , args) (* FIXME: what if the function appears in the body of the let? *) | GLetIn(_,nme,bdy,trm) , _ -> let _ = prstr "\nICI2 '!\n";Pp.flush_all() in let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in - GLetIn(dummy_loc,nme,bdy,newtrm) + GLetIn(Loc.ghost,nme,bdy,newtrm) | _, GLetIn(_,nme,bdy,trm) -> let _ = prstr "\nICI3 '!\n";Pp.flush_all() in let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in - GLetIn(dummy_loc,nme,bdy,newtrm) + GLetIn(Loc.ghost,nme,bdy,newtrm) | _ -> let _ = prstr "\nICI4 '!\n";Pp.flush_all() in raise NoMerge @@ -831,7 +831,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = let _ = prNamedRConstr (string_of_name nme) tp in let _ = prstr " ; " in let typ = glob_constr_to_constr_expr tp in - LocalRawAssum ([(dummy_loc,nme)], Constrexpr_ops.default_binder_kind, typ) :: acc) + LocalRawAssum ([(Loc.ghost,nme)], Constrexpr_ops.default_binder_kind, typ) :: acc) [] params in let concl = Constrextern.extern_constr false (Global.env()) concl in let arity,_ = @@ -839,7 +839,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = (fun (acc,env) (nm,_,c) -> let typ = Constrextern.extern_constr false env c in let newenv = Environ.push_rel (nm,None,c) env in - CProdN (dummy_loc, [[(dummy_loc,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv) + CProdN (Loc.ghost, [[(Loc.ghost,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv) (concl,Global.env()) (shift.funresprms2 @ shift.funresprms1 @ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in @@ -853,12 +853,12 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = FIXME: params et cstr_expr (arity) *) let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift (rawlist:(identifier * glob_constr) list) = - let lident = dummy_loc, shift.ident in + let lident = Loc.ghost, shift.ident in let bindlist , cstr_expr = (* params , arities *) merge_rec_params_and_arity prms1 prms2 shift mkSet in let lcstor_expr : (bool * (lident * constr_expr)) list = List.map (* zeta_normalize t ? *) - (fun (id,t) -> false, ((dummy_loc,id),glob_constr_to_constr_expr t)) + (fun (id,t) -> false, ((Loc.ghost,id),glob_constr_to_constr_expr t)) rawlist in lident , bindlist , Some cstr_expr , lcstor_expr @@ -868,7 +868,7 @@ let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) = match rdecl with | (nme,None,t) -> let traw = Detyping.detype false [] [] t in - GProd (dummy_loc,nme,Explicit,traw,t2) + GProd (Loc.ghost,nme,Explicit,traw,t2) | (_,Some _,_) -> assert false @@ -878,7 +878,7 @@ let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) = match rdecl with | (nme,None,t) -> let traw = Detyping.detype false [] [] t in - GProd (dummy_loc,nme,Explicit,traw,t2) + GProd (Loc.ghost,nme,Explicit,traw,t2) | (_,Some _,_) -> assert false @@ -915,7 +915,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive) (* Find infos on identifier id. *) let find_Function_infos_safe (id:identifier): Indfun_common.function_info = let kn_of_id x = - let f_ref = Libnames.Ident (dummy_loc,x) in + let f_ref = Libnames.Ident (Loc.ghost,x) in locate_with_msg (str "Don't know what to do with " ++ Libnames.pr_reference f_ref) locate_constant f_ref in try find_Function_infos (kn_of_id id) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index fe359f08d..af7ec6f20 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -189,7 +189,7 @@ let simpl_iter clause = (* Others ugly things ... *) let (value_f:constr list -> global_reference -> constr) = fun al fterm -> - let d0 = dummy_loc in + let d0 = Loc.ghost in let rev_x_id_l = ( List.fold_left @@ -861,8 +861,8 @@ let rec make_rewrite_list expr_info max = function general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true (mkVar hp, - ExplicitBindings[dummy_loc,NamedHyp def, - expr_info.f_constr;dummy_loc,NamedHyp k, + ExplicitBindings[Loc.ghost,NamedHyp def, + expr_info.f_constr;Loc.ghost,NamedHyp k, (f_S max)]) false g) ) ) [make_rewrite_list expr_info max l; @@ -888,8 +888,8 @@ let make_rewrite expr_info l hp max = (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true (mkVar hp, - ExplicitBindings[dummy_loc,NamedHyp def, - expr_info.f_constr;dummy_loc,NamedHyp k, + ExplicitBindings[Loc.ghost,NamedHyp def, + expr_info.f_constr;Loc.ghost,NamedHyp k, (f_S (f_S max))]) false) g) [observe_tac(str "make_rewrite finalize") ( (* tclORELSE( h_reflexivity) *) @@ -1279,7 +1279,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ Errors.error "\"abstract\" cannot handle existentials"; let hook _ _ = let opacity = - let na_ref = Libnames.Ident (dummy_loc,na) in + let na_ref = Libnames.Ident (Loc.ghost,na) in let na_global = Nametab.global na_ref in match na_global with ConstRef c -> is_opaque_constant c @@ -1512,7 +1512,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let hook _ _ = let term_ref = Nametab.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in - let _ = Table.extraction_inline true [Ident (dummy_loc,term_id)] in + let _ = Table.extraction_inline true [Ident (Loc.ghost,term_id)] in (* message "start second proof"; *) let stop = try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index 9698ca73a..87c9e1097 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -13,8 +13,8 @@ open Tacexpr open Quote let make_cont k x = - let k = TacDynamic(dummy_loc, Tacinterp.tactic_in (fun _ -> k)) in - let x = TacDynamic(dummy_loc, Pretyping.constr_in x) in + let k = TacDynamic(Loc.ghost, Tacinterp.tactic_in (fun _ -> k)) in + let x = TacDynamic(Loc.ghost, Pretyping.constr_in x) in let tac = <:tactic> in Tacinterp.interp tac diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 9b569a2b6..fea571f2e 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -136,18 +136,18 @@ END;;*) (* let closed_term_ast l = TacFun([Some(id_of_string"t")], - TacAtom(dummy_loc,TacExtend(dummy_loc,"closed_term", + TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term", [Genarg.in_gen Genarg.wit_constr (mkVar(id_of_string"t")); Genarg.in_gen (Genarg.wit_list1 Genarg.wit_ref) l]))) *) let closed_term_ast l = - let l = List.map (fun gr -> ArgArg(dummy_loc,gr)) l in + let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in TacFun([Some(id_of_string"t")], - TacAtom(dummy_loc,TacExtend(dummy_loc,"closed_term", - [Genarg.in_gen Genarg.globwit_constr (GVar(dummy_loc,id_of_string"t"),None); + TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term", + [Genarg.in_gen Genarg.globwit_constr (GVar(Loc.ghost,id_of_string"t"),None); Genarg.in_gen (Genarg.wit_list1 Genarg.globwit_ref) l]))) (* -let _ = add_tacdef false ((dummy_loc,id_of_string"ring_closed_term" +let _ = add_tacdef false ((Loc.ghost,id_of_string"ring_closed_term" *) (****************************************************************************) @@ -168,14 +168,14 @@ let decl_constant na c = (* Calling a global tactic *) let ltac_call tac (args:glob_tactic_arg list) = - TacArg(dummy_loc,TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args)) + TacArg(Loc.ghost,TacCall(Loc.ghost, ArgArg(Loc.ghost, Lazy.force tac),args)) (* Calling a locally bound tactic *) let ltac_lcall tac args = - TacArg(dummy_loc,TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args)) + TacArg(Loc.ghost,TacCall(Loc.ghost, ArgVar(Loc.ghost, id_of_string tac),args)) let ltac_letin (x, e1) e2 = - TacLetIn(false,[(dummy_loc,id_of_string x),e1],e2) + TacLetIn(false,[(Loc.ghost,id_of_string x),e1],e2) let ltac_apply (f:glob_tactic_expr) (args:glob_tactic_arg list) = Tacinterp.eval_tactic @@ -185,7 +185,7 @@ let ltac_record flds = TacFun([Some(id_of_string"proj")], ltac_lcall "proj" flds) -let carg c = TacDynamic(dummy_loc,Pretyping.constr_in c) +let carg c = TacDynamic(Loc.ghost,Pretyping.constr_in c) let dummy_goal env = let (gl,_,sigma) = @@ -627,24 +627,24 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac = | None -> (match rk, opp, kind with Abstract, None, _ -> - let t = ArgArg(dummy_loc,Lazy.force ltac_inv_morphN) in - TacArg(dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul])) + let t = ArgArg(Loc.ghost,Lazy.force ltac_inv_morphN) in + TacArg(Loc.ghost,TacCall(Loc.ghost,t,List.map carg [zero;one;add;mul])) | Abstract, Some opp, Some _ -> - let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphZ) in - TacArg(dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) + let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morphZ) in + TacArg(Loc.ghost,TacCall(Loc.ghost,t,List.map carg [zero;one;add;mul;opp])) | Abstract, Some opp, None -> - let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphNword) in + let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morphNword) in TacArg - (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) + (Loc.ghost,TacCall(Loc.ghost,t,List.map carg [zero;one;add;mul;opp])) | Computational _,_,_ -> - let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in + let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_gen) in TacArg - (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;zero;one])) + (Loc.ghost,TacCall(Loc.ghost,t,List.map carg [zero;one;zero;one])) | Morphism mth,_,_ -> let (_,czero,cone,_,_,_,_,_,_) = dest_morph env sigma mth in - let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in + let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_gen) in TacArg - (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;czero;cone]))) + (Loc.ghost,TacCall(Loc.ghost,t,List.map carg [zero;one;czero;cone]))) let make_hyp env c = let t = Retyping.get_type_of env Evd.empty c in @@ -660,8 +660,8 @@ let interp_power env pow = let carrier = Lazy.force coq_hypo in match pow with | None -> - let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_nothing) in - (TacArg(dummy_loc,TacCall(dummy_loc,t,[])), lapp coq_None [|carrier|]) + let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_nothing) in + (TacArg(Loc.ghost,TacCall(Loc.ghost,t,[])), lapp coq_None [|carrier|]) | Some (tac, spec) -> let tac = match tac with diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index b2e2e5b19..17dd563f7 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -80,4 +80,4 @@ let _ = Notation.declare_string_interpreter "char_scope" (ascii_path,ascii_module) interp_ascii_string - ([GRef (dummy_loc,static_glob_Ascii)], uninterp_ascii_string, true) + ([GRef (Loc.ghost,static_glob_Ascii)], uninterp_ascii_string, true) diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index 5a355b971..2fb8ce451 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -75,4 +75,4 @@ let _ = Notation.declare_numeral_interpreter "nat_scope" (nat_path,["Coq";"Init";"Datatypes"]) nat_of_int - ([GRef (dummy_loc,glob_S); GRef (dummy_loc,glob_O)], uninterp_nat, true) + ([GRef (Loc.ghost,glob_S); GRef (Loc.ghost,glob_O)], uninterp_nat, true) diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index b67cbb934..97753951a 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -144,7 +144,7 @@ let uninterp_int31 i = let _ = Notation.declare_numeral_interpreter int31_scope (int31_path, int31_module) interp_int31 - ([GRef (Pp.dummy_loc, int31_construct)], + ([GRef (Loc.ghost, int31_construct)], uninterp_int31, true) @@ -258,7 +258,7 @@ let uninterp_bigN rc = let bigN_list_of_constructors = let rec build i = if less_than i (add_1 n_inlined) then - GRef (Pp.dummy_loc, bigN_constructor i)::(build (add_1 i)) + GRef (Loc.ghost, bigN_constructor i)::(build (add_1 i)) else [] in @@ -304,8 +304,8 @@ let uninterp_bigZ rc = let _ = Notation.declare_numeral_interpreter bigZ_scope (bigZ_path, bigZ_module) interp_bigZ - ([GRef (Pp.dummy_loc, bigZ_pos); - GRef (Pp.dummy_loc, bigZ_neg)], + ([GRef (Loc.ghost, bigZ_pos); + GRef (Loc.ghost, bigZ_neg)], uninterp_bigZ, true) @@ -325,5 +325,5 @@ let uninterp_bigQ rc = let _ = Notation.declare_numeral_interpreter bigQ_scope (bigQ_path, bigQ_module) interp_bigQ - ([GRef (Pp.dummy_loc, bigQ_z)], uninterp_bigQ, + ([GRef (Loc.ghost, bigQ_z)], uninterp_bigQ, true) diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index f8161c52f..4e0a206dd 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -118,8 +118,8 @@ let uninterp_r p = let _ = Notation.declare_numeral_interpreter "R_scope" (r_path,["Coq";"Reals";"Rdefinitions"]) r_of_int - ([GRef(dummy_loc,glob_Ropp);GRef(dummy_loc,glob_R0); - GRef(dummy_loc,glob_Rplus);GRef(dummy_loc,glob_Rmult); - GRef(dummy_loc,glob_R1)], + ([GRef(Loc.ghost,glob_Ropp);GRef(Loc.ghost,glob_R0); + GRef(Loc.ghost,glob_Rplus);GRef(Loc.ghost,glob_Rmult); + GRef(Loc.ghost,glob_R1)], uninterp_r, false) diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index ac17492d2..7474a8b0e 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -64,6 +64,6 @@ let _ = Notation.declare_string_interpreter "string_scope" (string_path,["Coq";"Strings";"String"]) interp_string - ([GRef (dummy_loc,static_glob_String); - GRef (dummy_loc,static_glob_EmptyString)], + ([GRef (Loc.ghost,static_glob_String); + GRef (Loc.ghost,static_glob_EmptyString)], uninterp_string, true) diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index a69ec9ed1..e461ea152 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -87,9 +87,9 @@ let uninterp_positive p = let _ = Notation.declare_numeral_interpreter "positive_scope" (positive_path,binnums) interp_positive - ([GRef (dummy_loc, glob_xI); - GRef (dummy_loc, glob_xO); - GRef (dummy_loc, glob_xH)], + ([GRef (Loc.ghost, glob_xI); + GRef (Loc.ghost, glob_xO); + GRef (Loc.ghost, glob_xH)], uninterp_positive, true) @@ -138,8 +138,8 @@ let uninterp_n p = let _ = Notation.declare_numeral_interpreter "N_scope" (n_path,binnums) n_of_int - ([GRef (dummy_loc, glob_N0); - GRef (dummy_loc, glob_Npos)], + ([GRef (Loc.ghost, glob_N0); + GRef (Loc.ghost, glob_Npos)], uninterp_n, true) @@ -186,8 +186,8 @@ let uninterp_z p = let _ = Notation.declare_numeral_interpreter "Z_scope" (z_path,binnums) z_of_int - ([GRef (dummy_loc, glob_ZERO); - GRef (dummy_loc, glob_POS); - GRef (dummy_loc, glob_NEG)], + ([GRef (Loc.ghost, glob_ZERO); + GRef (Loc.ghost, glob_POS); + GRef (Loc.ghost, glob_NEG)], uninterp_z, true) -- cgit v1.2.3