diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-22 15:14:30 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-22 15:14:30 +0000 |
| commit | 6b45f2d36929162cf92272bb60c2c245d9a0ead3 (patch) | |
| tree | 93aa975697b7de73563c84773d99b4c65b92173b | |
| parent | fea214f82954197d23fda9a0e4e7d93e0cbf9b4c (diff) | |
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
168 files changed, 803 insertions, 750 deletions
diff --git a/Makefile.common b/Makefile.common index a9a87e2f0..5ce5442f8 100644 --- a/Makefile.common +++ b/Makefile.common @@ -229,7 +229,7 @@ IDEMOD:=$(shell cat ide/ide.mllib) # coqmktop, coqc COQENVCMO:=lib/clib.cma\ - lib/pp_control.cmo lib/compat.cmo lib/pp.cmo lib/errors.cmo + lib/pp_control.cmo lib/compat.cmo lib/pp.cmo lib/loc.cmo lib/errors.cmo COQMKTOPCMO:=$(COQENVCMO) scripts/tolink.cmo scripts/coqmktop.cmo diff --git a/checker/check.mllib b/checker/check.mllib index 2cd86355f..15d7df1d3 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -3,6 +3,7 @@ Pp_control Compat Flags Pp +Loc Segmenttree Unicodetable Errors diff --git a/checker/checker.ml b/checker/checker.ml index 53c059eb3..15c27ffa5 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Compat open Pp open Errors open Util @@ -215,10 +214,10 @@ let anomaly_string () = str "Anomaly: " let report () = (str "." ++ spc () ++ str "Please report.") let print_loc loc = - if loc = dummy_loc then + if loc = Loc.ghost then (str"<unknown>") else - let loc = unloc loc in + let loc = Loc.unloc loc in (int (fst loc) ++ str"-" ++ int (snd loc)) let guill s = "\""^s^"\"" @@ -274,7 +273,7 @@ let rec explain_exn = function hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error ctx e)*) | Loc.Exc_located (loc,exc) -> - hov 0 ((if loc = dummy_loc then (mt ()) + hov 0 ((if loc = Loc.ghost then (mt ()) else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) ++ explain_exn exc) | Assert_failure (s,b,e) -> diff --git a/checker/modops.ml b/checker/modops.ml index 4212a9361..1a7d57e1c 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -37,7 +37,7 @@ let error_no_such_label_sub l l1 = let error_not_a_module_loc loc s = user_err_loc (loc,"",str ("\""^string_of_label s^"\" is not a module")) -let error_not_a_module s = error_not_a_module_loc dummy_loc s +let error_not_a_module s = error_not_a_module_loc Loc.ghost s let error_with_incorrect l = error ("Incorrect constraint for label \""^(string_of_label l)^"\"") diff --git a/dev/printers.mllib b/dev/printers.mllib index 03d62e207..a6d93aa8c 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -4,6 +4,7 @@ Pp_control Compat Flags Pp +Loc Segmenttree Unicodetable Errors diff --git a/dev/top_printers.ml b/dev/top_printers.ml index b3ede70bf..570ad59ff 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -353,7 +353,7 @@ let print_pure_constr csr = let ppfconstr c = ppconstr (Closure.term_of_fconstr c) -let pploc x = let (l,r) = unloc x in +let pploc x = let (l,r) = Loc.unloc x in print_string"(";print_int l;print_string",";print_int r;print_string")" (* extendable tactic arguments *) @@ -428,7 +428,7 @@ let _ = extend_vernac_command_grammar "PrintConstr" None [[GramTerminal "PrintConstr"; GramNonTerminal - (dummy_loc,ConstrArgType,Aentry ("constr","constr"), + (Loc.ghost,ConstrArgType,Aentry ("constr","constr"), Some (Names.id_of_string "c"))]] let _ = @@ -445,7 +445,7 @@ let _ = extend_vernac_command_grammar "PrintPureConstr" None [[GramTerminal "PrintPureConstr"; GramNonTerminal - (dummy_loc,ConstrArgType,Aentry ("constr","constr"), + (Loc.ghost,ConstrArgType,Aentry ("constr","constr"), Some (Names.id_of_string "c"))]] (* Setting printer of unbound global reference *) diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index a13059799..1f9304ddd 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -14,8 +14,8 @@ open Egramml open Pcoq open Compat -let loc = Pp.dummy_loc -let default_loc = <:expr< Pp.dummy_loc >> +let loc = Loc.ghost +let default_loc = <:expr< Loc.ghost >> let rec make_rawwit loc = function | BoolArgType -> <:expr< Genarg.rawwit_bool >> diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 5ab3057fe..006766e17 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -4,6 +4,7 @@ Pp_control Compat Flags Pp +Loc Segmenttree Unicodetable Errors diff --git a/grammar/q_constr.ml4 b/grammar/q_constr.ml4 index fe4ccc53d..7a36c7b78 100644 --- a/grammar/q_constr.ml4 +++ b/grammar/q_constr.ml4 @@ -19,8 +19,8 @@ open Pcaml open PcamlSig open Misctypes -let loc = dummy_loc -let dloc = <:expr< Pp.dummy_loc >> +let loc = Loc.ghost +let dloc = <:expr< Loc.ghost >> let apply_ref f l = <:expr< diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index 7467a32f0..c202664e2 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -21,9 +21,9 @@ let anti loc x = expl_anti loc <:expr< $lid:purge_str x$ >> (* We don't give location for tactic quotation! *) -let loc = dummy_loc +let loc = Loc.ghost -let dloc = <:expr< Pp.dummy_loc >> +let dloc = <:expr< Loc.ghost >> let mlexpr_of_ident id = <:expr< Names.id_of_string $str:Names.string_of_id id$ >> diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index cfaa2a654..44dd4941a 100644 --- a/grammar/q_util.ml4 +++ b/grammar/q_util.ml4 @@ -16,27 +16,27 @@ let mlexpr_of_list f l = List.fold_right (fun e1 e2 -> let e1 = f e1 in - let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in + let loc = Loc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in <:expr< [$e1$ :: $e2$] >>) - l (let loc = dummy_loc in <:expr< [] >>) + l (let loc = Loc.ghost in <:expr< [] >>) let mlexpr_of_pair m1 m2 (a1,a2) = let e1 = m1 a1 and e2 = m2 a2 in - let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in + let loc = Loc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in <:expr< ($e1$, $e2$) >> let mlexpr_of_triple m1 m2 m3 (a1,a2,a3)= let e1 = m1 a1 and e2 = m2 a2 and e3 = m3 a3 in - let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e3) in + let loc = Loc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e3) in <:expr< ($e1$, $e2$, $e3$) >> let mlexpr_of_quadruple m1 m2 m3 m4 (a1,a2,a3,a4)= let e1 = m1 a1 and e2 = m2 a2 and e3 = m3 a3 and e4 = m4 a4 in - let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e4) in + let loc = Loc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e4) in <:expr< ($e1$, $e2$, $e3$, $e4$) >> (* We don't give location for tactic quotation! *) -let loc = dummy_loc +let loc = Loc.ghost let mlexpr_of_bool = function diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 06c3ac3f9..8f70302a0 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -31,7 +31,7 @@ let rec make_when loc = function | GramNonTerminal(loc',t,_,Some p)::l -> let p = Names.string_of_id p in let l = make_when loc l in - let loc = join_loc loc' loc in + let loc = Loc.merge loc' loc in let t = mlexpr_of_argtype loc' t in <:expr< Genarg.genarg_tag $lid:p$ = $t$ && $l$ >> | _::l -> make_when loc l @@ -40,7 +40,7 @@ let rec make_let e = function | [] -> e | GramNonTerminal(loc,t,_,Some p)::l -> let p = Names.string_of_id p in - let loc = join_loc loc (MLast.loc_of_expr e) in + let loc = Loc.merge loc (MLast.loc_of_expr e) in let e = make_let e l in let v = <:expr< Genarg.out_gen $make_wit loc t$ $lid:p$ >> in <:expr< let $lid:p$ = $v$ in $e$ >> @@ -78,7 +78,7 @@ let rec make_eval_tactic e = function | [] -> e | GramNonTerminal(loc,tag,_,Some p)::l when is_tactic_genarg tag -> let p = Names.string_of_id p in - let loc = join_loc loc (MLast.loc_of_expr e) in + let loc = Loc.merge loc (MLast.loc_of_expr e) in let e = make_eval_tactic e l in <:expr< let $lid:p$ = $lid:p$ in $e$ >> | _::l -> make_eval_tactic e l @@ -107,7 +107,7 @@ let rec make_tags loc = function | [] -> <:expr< [] >> | GramNonTerminal(loc',t,_,Some p)::l -> let l = make_tags loc l in - let loc = join_loc loc' loc in + let loc = Loc.merge loc' loc in let t = mlexpr_of_argtype loc' t in <:expr< [ $t$ :: $l$ ] >> | _::l -> make_tags loc l diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index b66460fe6..8ec189e3d 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -23,7 +23,7 @@ let rec make_let e = function | [] -> e | GramNonTerminal(loc,t,_,Some p)::l -> let p = Names.string_of_id p in - let loc = join_loc loc (MLast.loc_of_expr e) in + let loc = Loc.merge loc (MLast.loc_of_expr e) in let e = make_let e l in <:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >> | _::l -> make_let e l diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 27cebf9e6..282b2c733 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -74,43 +74,43 @@ let raw_cases_pattern_expr_loc = function let local_binder_loc = function | LocalRawAssum ((loc,_)::_,_,t) - | LocalRawDef ((loc,_),t) -> join_loc loc (constr_loc t) + | LocalRawDef ((loc,_),t) -> Loc.merge loc (constr_loc t) | LocalRawAssum ([],_,_) -> assert false let local_binders_loc bll = - if bll = [] then dummy_loc else - join_loc (local_binder_loc (List.hd bll)) (local_binder_loc (list_last bll)) + if bll = [] then Loc.ghost else + Loc.merge (local_binder_loc (List.hd bll)) (local_binder_loc (list_last bll)) (** Pseudo-constructors *) -let mkIdentC id = CRef (Ident (dummy_loc, id)) +let mkIdentC id = CRef (Ident (Loc.ghost, id)) let mkRefC r = CRef r -let mkCastC (a,k) = CCast (dummy_loc,a,k) -let mkLambdaC (idl,bk,a,b) = CLambdaN (dummy_loc,[idl,bk,a],b) -let mkLetInC (id,a,b) = CLetIn (dummy_loc,id,a,b) -let mkProdC (idl,bk,a,b) = CProdN (dummy_loc,[idl,bk,a],b) +let mkCastC (a,k) = CCast (Loc.ghost,a,k) +let mkLambdaC (idl,bk,a,b) = CLambdaN (Loc.ghost,[idl,bk,a],b) +let mkLetInC (id,a,b) = CLetIn (Loc.ghost,id,a,b) +let mkProdC (idl,bk,a,b) = CProdN (Loc.ghost,[idl,bk,a],b) let mkAppC (f,l) = let l = List.map (fun x -> (x,None)) l in match f with - | CApp (_,g,l') -> CApp (dummy_loc, g, l' @ l) - | _ -> CApp (dummy_loc, (None, f), l) + | CApp (_,g,l') -> CApp (Loc.ghost, g, l' @ l) + | _ -> CApp (Loc.ghost, (None, f), l) let rec mkCProdN loc bll c = match bll with | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll -> - CProdN (loc,[idl,bk,t],mkCProdN (join_loc loc1 loc) bll c) + CProdN (loc,[idl,bk,t],mkCProdN (Loc.merge loc1 loc) bll c) | LocalRawDef ((loc1,_) as id,b) :: bll -> - CLetIn (loc,id,b,mkCProdN (join_loc loc1 loc) bll c) + CLetIn (loc,id,b,mkCProdN (Loc.merge loc1 loc) bll c) | [] -> c | LocalRawAssum ([],_,_) :: bll -> mkCProdN loc bll c let rec mkCLambdaN loc bll c = match bll with | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll -> - CLambdaN (loc,[idl,bk,t],mkCLambdaN (join_loc loc1 loc) bll c) + CLambdaN (loc,[idl,bk,t],mkCLambdaN (Loc.merge loc1 loc) bll c) | LocalRawDef ((loc1,_) as id,b) :: bll -> - CLetIn (loc,id,b,mkCLambdaN (join_loc loc1 loc) bll c) + CLetIn (loc,id,b,mkCLambdaN (Loc.merge loc1 loc) bll c) | [] -> c | LocalRawAssum ([],_,_) :: bll -> mkCLambdaN loc bll c diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index d3e32da46..a90a31950 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Loc open Pp open Names open Libnames @@ -16,12 +17,12 @@ open Constrexpr (** Constrexpr_ops: utilities on [constr_expr] *) -val constr_loc : constr_expr -> loc +val constr_loc : constr_expr -> Loc.t -val cases_pattern_expr_loc : cases_pattern_expr -> loc -val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> loc +val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t +val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t -val local_binders_loc : local_binder list -> loc +val local_binders_loc : local_binder list -> Loc.t val default_binder_kind : binder_kind @@ -41,8 +42,8 @@ val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr val prod_constr_expr : constr_expr -> local_binder list -> constr_expr (** Same as [abstract_constr_expr] and [prod_constr_expr], with location *) -val mkCLambdaN : loc -> local_binder list -> constr_expr -> constr_expr -val mkCProdN : loc -> local_binder list -> constr_expr -> constr_expr +val mkCLambdaN : Loc.t -> local_binder list -> constr_expr -> constr_expr +val mkCProdN : Loc.t -> local_binder list -> constr_expr -> constr_expr (** For binders parsing *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index c90bbf4f8..86308b6a0 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -130,7 +130,7 @@ module PrintingConstructor = Goptions.MakeRefTable(PrintingRecordConstructor) let insert_delimiters e = function | None -> e - | Some sc -> CDelimiters (dummy_loc,sc,e) + | Some sc -> CDelimiters (Loc.ghost,sc,e) let insert_pat_delimiters loc p = function | None -> p @@ -220,7 +220,7 @@ let rec check_same_type ty1 ty2 = | CCases(_,_,_,a1,brl1), CCases(_,_,_,a2,brl2) -> List.iter2 (fun (tm1,_) (tm2,_) -> check_same_type tm1 tm2) a1 a2; List.iter2 (fun (_,pl1,r1) (_,pl2,r2) -> - List.iter2 (located_iter2 (List.iter2 check_same_pattern)) pl1 pl2; + List.iter2 (Loc.located_iter2 (List.iter2 check_same_pattern)) pl1 pl2; check_same_type r1 r2) brl1 brl2 | CHole _, CHole _ -> () | CPatVar(_,i1), CPatVar(_,i2) when i1=i2 -> () @@ -260,7 +260,7 @@ let same c d = try check_same_type c d; true with _ -> false (* mapping patterns to cases_pattern_expr *) let add_patt_for_params ind l = - Util.list_addn (fst (Inductiveops.inductive_nargs ind)) (CPatAtom (dummy_loc,None)) l + Util.list_addn (fst (Inductiveops.inductive_nargs ind)) (CPatAtom (Loc.ghost,None)) l let drop_implicits_in_patt cst nb_expl args = let impl_st = (implicits_of_global cst) in @@ -485,7 +485,7 @@ let rec extern_symbol_ind_pattern allscopes vars ind args = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> try - apply_notation_to_pattern dummy_loc (IndRef ind) + apply_notation_to_pattern Loc.ghost (IndRef ind) (match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule with No_match -> extern_symbol_ind_pattern allscopes vars ind args rules @@ -494,9 +494,9 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = (* pboutill: There are letins in pat which is incompatible with notations and not explicit application. *) if !in_debugger||Inductiveops.inductive_has_local_defs ind then - let c = extern_reference dummy_loc vars (IndRef ind) in + let c = extern_reference Loc.ghost vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in - CPatCstr (dummy_loc, c, add_patt_for_params ind args, []) + CPatCstr (Loc.ghost, c, add_patt_for_params ind args, []) else try if !Flags.raw_print or !print_no_symbol then raise No_match; @@ -504,18 +504,18 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = match availability_of_prim_token p sc scopes with | None -> raise No_match | Some key -> - insert_pat_delimiters dummy_loc (CPatPrim(dummy_loc,p)) key + insert_pat_delimiters Loc.ghost (CPatPrim(Loc.ghost,p)) key with No_match -> try if !Flags.raw_print or !print_no_symbol then raise No_match; extern_symbol_ind_pattern scopes vars ind args (uninterp_ind_pattern_notations ind) with No_match -> - let c = extern_reference dummy_loc vars (IndRef ind) in + let c = extern_reference Loc.ghost vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in match drop_implicits_in_patt (IndRef ind) 0 args with - |Some true_args -> CPatCstr (dummy_loc, c, [], true_args) - |None -> CPatCstr (dummy_loc, c, args, []) + |Some true_args -> CPatCstr (Loc.ghost, c, [], true_args) + |None -> CPatCstr (Loc.ghost, c, args, []) let extern_cases_pattern vars p = extern_cases_pattern_in_scope (None,[]) vars p @@ -561,7 +561,7 @@ let explicitize loc inctx impl (cf,f) args = not (is_inferable_implicit inctx n imp)) in if visible then - (a,Some (dummy_loc, ExplByName (name_of_implicit imp))) :: tail + (a,Some (Loc.ghost, ExplByName (name_of_implicit imp))) :: tail else tail | a::args, _::impl -> (a,None) :: exprec (q+1) (args,impl) @@ -756,12 +756,12 @@ let rec extern inctx scopes vars r = | GProd (loc,na,bk,t,c) -> let t = extern_typ scopes vars (anonymize_if_reserved na t) in let (idl,c) = factorize_prod scopes (add_vname vars na) t c in - CProdN (loc,[(dummy_loc,na)::idl,Default bk,t],c) + CProdN (loc,[(Loc.ghost,na)::idl,Default bk,t],c) | GLambda (loc,na,bk,t,c) -> let t = extern_typ scopes vars (anonymize_if_reserved na t) in let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in - CLambdaN (loc,[(dummy_loc,na)::idl,Default bk,t],c) + CLambdaN (loc,[(Loc.ghost,na)::idl,Default bk,t],c) | GCases (loc,sty,rtntypopt,tml,eqns) -> let vars' = @@ -772,13 +772,13 @@ let rec extern inctx scopes vars r = let na' = match na,tm with Anonymous, GVar (_,id) when rtntypopt<>None & occur_glob_constr id (Option.get rtntypopt) - -> Some (dummy_loc,Anonymous) + -> Some (Loc.ghost,Anonymous) | Anonymous, _ -> None | Name id, GVar (_,id') when id=id' -> None - | Name _, _ -> Some (dummy_loc,na) in + | Name _, _ -> Some (Loc.ghost,na) in (sub_extern false scopes vars tm, (na',Option.map (fun (loc,ind,nal) -> - let args = List.map (fun x -> PatVar (dummy_loc, x)) nal in + let args = List.map (fun x -> PatVar (Loc.ghost, x)) nal in let fullargs = Notation_ops.add_patterns_for_params ind args in extern_ind_pattern_in_scope scopes vars ind fullargs ) x))) tml in @@ -786,15 +786,15 @@ let rec extern inctx scopes vars r = CCases (loc,sty,rtntypopt',tml,eqns) | GLetTuple (loc,nal,(na,typopt),tm,b) -> - CLetTuple (loc,List.map (fun na -> (dummy_loc,na)) nal, - (Option.map (fun _ -> (dummy_loc,na)) typopt, + CLetTuple (loc,List.map (fun na -> (Loc.ghost,na)) nal, + (Option.map (fun _ -> (Loc.ghost,na)) typopt, Option.map (extern_typ scopes (add_vname vars na)) typopt), sub_extern false scopes vars tm, extern inctx scopes (List.fold_left add_vname vars nal) b) | GIf (loc,c,(na,typopt),b1,b2) -> CIf (loc,sub_extern false scopes vars c, - (Option.map (fun _ -> (dummy_loc,na)) typopt, + (Option.map (fun _ -> (Loc.ghost,na)) typopt, Option.map (extern_typ scopes (add_vname vars na)) typopt), sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2) @@ -811,10 +811,10 @@ let rec extern inctx scopes vars r = let n = match fst nv.(i) with | None -> None - | Some x -> Some (dummy_loc, out_name (List.nth assums x)) + | Some x -> Some (Loc.ghost, out_name (List.nth assums x)) in let ro = extern_recursion_order scopes vars (snd nv.(i)) in - ((dummy_loc, fi), (n, ro), bl, extern_typ scopes vars0 ty, + ((Loc.ghost, fi), (n, ro), bl, extern_typ scopes vars0 ty, extern false scopes vars1 def)) idv in CFix (loc,(loc,idv.(n)),Array.to_list listdecl) @@ -824,7 +824,7 @@ let rec extern inctx scopes vars r = let (_,ids,bl) = extern_local_binder scopes vars blv.(i) in let vars0 = List.fold_right (name_fold Idset.add) ids vars in let vars1 = List.fold_right (name_fold Idset.add) ids vars' in - ((dummy_loc, fi),bl,extern_typ scopes vars0 tyv.(i), + ((Loc.ghost, fi),bl,extern_typ scopes vars0 tyv.(i), sub_extern false scopes vars1 bv.(i))) idv in CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl)) @@ -873,7 +873,7 @@ and extern_local_binder scopes vars = function let (assums,ids,l) = extern_local_binder scopes (name_fold Idset.add na vars) l in (assums,na::ids, - LocalRawDef((dummy_loc,na), extern false scopes vars bd) :: l) + LocalRawDef((Loc.ghost,na), extern false scopes vars bd) :: l) | (na,bk,None,ty)::l -> let ty = extern_typ scopes vars (anonymize_if_reserved na ty) in @@ -883,10 +883,10 @@ and extern_local_binder scopes vars = function match na with Name id -> not (occur_var_constr_expr id ty') | _ -> true -> (na::assums,na::ids, - LocalRawAssum((dummy_loc,na)::nal,k,ty')::l) + LocalRawAssum((Loc.ghost,na)::nal,k,ty')::l) | (assums,ids,l) -> (na::assums,na::ids, - LocalRawAssum([(dummy_loc,na)],Default bk,ty) :: l)) + LocalRawAssum([(Loc.ghost,na)],Default bk,ty) :: l)) and extern_eqn inctx scopes vars (loc,ids,pl,c) = (loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl], @@ -915,7 +915,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function subscopes,impls | _ -> [], [] in - (if n = 0 then f else GApp (dummy_loc,f,args1)), + (if n = 0 then f else GApp (Loc.ghost,f,args1)), args2, subscopes, impls | GApp (_,(GRef (_,ref) as f),args), None -> let subscopes = find_arguments_scope ref in @@ -923,7 +923,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function select_impargs_size (List.length args) (implicits_of_global ref) in f, args, subscopes, impls - | GRef _, Some 0 -> GApp (dummy_loc,t,[]), [], [], [] + | GRef _, Some 0 -> GApp (Loc.ghost,t,[]), [], [], [] | _, None -> t, [], [], [] | _ -> raise No_match in (* Try matching ... *) @@ -983,7 +983,7 @@ let extern_glob_type vars c = (******************************************************************) (* Main translation function from constr -> constr_expr *) -let loc = dummy_loc (* for constr and pattern, locations are lost *) +let loc = Loc.ghost (* for constr and pattern, locations are lost *) let extern_constr_gen goal_concl_style scopt env t = (* "goal_concl_style" means do alpha-conversion using the "goal" convention *) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 0c5d4b589..9f7acbc6d 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -37,7 +37,7 @@ val extern_constr_pattern : names_context -> constr_pattern -> constr_expr val extern_constr : bool -> env -> constr -> constr_expr val extern_constr_in_scope : bool -> scope_name -> env -> constr -> constr_expr -val extern_reference : loc -> Idset.t -> global_reference -> reference +val extern_reference : Loc.t -> Idset.t -> global_reference -> reference val extern_type : bool -> env -> types -> constr_expr val extern_sort : sorts -> glob_sort val extern_rel_context : constr option -> env -> @@ -55,7 +55,7 @@ val print_projections : bool ref (** Debug printing options *) val set_debug_global_reference_printer : - (loc -> global_reference -> reference) -> unit + (Loc.t -> global_reference -> reference) -> unit val in_debugger : bool ref (** This governs printing of implicit arguments. If [with_implicits] is diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f6513fd0d..880afe57d 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -119,7 +119,7 @@ type internalization_error = | BadPatternsNumber of int * int | BadExplicitationNumber of explicitation * int option -exception InternalizationError of loc * internalization_error +exception InternalizationError of Loc.t * internalization_error let explain_variable_capture id id' = pr_id id ++ str " is dependent in the type of " ++ pr_id id' ++ @@ -325,12 +325,12 @@ let reset_tmp_scope env = {env with tmp_scope = None} let rec it_mkGProd loc2 env body = match env with - (loc1, (na, bk, _, t)) :: tl -> it_mkGProd loc2 tl (GProd (join_loc loc1 loc2, na, bk, t, body)) + (loc1, (na, bk, _, t)) :: tl -> it_mkGProd loc2 tl (GProd (Loc.merge loc1 loc2, na, bk, t, body)) | [] -> body let rec it_mkGLambda loc2 env body = match env with - (loc1, (na, bk, _, t)) :: tl -> it_mkGLambda loc2 tl (GLambda (join_loc loc1 loc2, na, bk, t, body)) + (loc1, (na, bk, _, t)) :: tl -> it_mkGLambda loc2 tl (GLambda (Loc.merge loc1 loc2, na, bk, t, body)) | [] -> body (**********************************************************************) @@ -474,10 +474,10 @@ let intern_generalization intern env lvar loc bk ak c = in if pi then (fun (id, loc') acc -> - GProd (join_loc loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id)), acc)) + GProd (Loc.merge loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id)), acc)) else (fun (id, loc') acc -> - GLambda (join_loc loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id)), acc)) + GLambda (Loc.merge loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id)), acc)) in List.fold_right (fun (id, loc as lid) (env, acc) -> let env' = push_name_env lvar (Variable,[],[],[]) env (loc, Name id) in @@ -738,7 +738,7 @@ let intern_applied_reference intern env namedctx lvar args = function let interp_reference vars r = let (r,_,_,_),_ = - intern_applied_reference (fun _ -> error_not_enough_arguments dummy_loc) + intern_applied_reference (fun _ -> error_not_enough_arguments Loc.ghost) {ids = Idset.empty; unb = false ; tmp_scope = None; scopes = []; impls = empty_internalization_env} [] (vars,[]) [] r @@ -800,7 +800,7 @@ let rec has_duplicate = function | x::l -> if List.mem x l then (Some x) else has_duplicate l let loc_of_lhs lhs = - join_loc (fst (List.hd lhs)) (fst (list_last lhs)) + Loc.merge (fst (List.hd lhs)) (fst (list_last lhs)) let check_linearity lhs ids = match has_duplicate ids with @@ -840,10 +840,10 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 else args_len = nargs_with_letin || (fst (fail (nargs - List.length impl_list + i)))) ,l) |imp::q as il,[] -> if is_status_implicit imp && maximal_insertion_of imp - then let (b,out) = aux i (q,[]) in (b,RCPatAtom(dummy_loc,None)::out) + then let (b,out) = aux i (q,[]) in (b,RCPatAtom(Loc.ghost,None)::out) else fail (remaining_args (len_pl1+i) il) |imp::q,(hh::tt as l) -> if is_status_implicit imp - then let (b,out) = aux i (q,l) in (b,RCPatAtom(dummy_loc,None)::out) + then let (b,out) = aux i (q,l) in (b,RCPatAtom(Loc.ghost,None)::out) else let (b,out) = aux (succ i) (q,tt) in (b,hh::out) in aux 0 (impl_list,pl2) @@ -883,7 +883,7 @@ let find_constructor loc add_params ref = |Some nb_args -> let nb = if nb_args = Inductiveops.constructor_nrealhyps c then fst (Inductiveops.inductive_nargs ind) else Inductiveops.inductive_nparams ind in - Util.list_make nb ([],[([],PatVar(dummy_loc,Anonymous))]) + Util.list_make nb ([],[([],PatVar(Loc.ghost,Anonymous))]) |None -> []) cstr let find_pattern_variable = function @@ -1312,7 +1312,7 @@ let internalize sigma globalenv env allow_patvar lvar c = let (_,bli,tyi,_) = idl_temp.(i) in let fix_args = (List.map (fun (_,(na, bk, _, _)) -> (build_impls bk na)) bli) in push_name_env lvar (impls_type_list ~args:fix_args tyi) - en (dummy_loc, Name name)) 0 env' lf in + en (Loc.ghost, Name name)) 0 env' lf in (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in GRec (loc,GFix (Array.map (fun (ro,_,_,_) -> ro) idl,n), @@ -1339,7 +1339,7 @@ let internalize sigma globalenv env allow_patvar lvar c = let (bli,tyi,_) = idl_tmp.(i) in let cofix_args = List.map (fun (_, (na, bk, _, _)) -> (build_impls bk na)) bli in push_name_env lvar (impls_type_list ~args:cofix_args tyi) - en (dummy_loc, Name name)) 0 env' lf in + en (Loc.ghost, Name name)) 0 env' lf in (b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in GRec (loc,GCoFix n, Array.of_list lf, @@ -1396,7 +1396,7 @@ let internalize sigma globalenv env allow_patvar lvar c = check_projection isproj (List.length args) c; (match c with (* Now compact "(f args') args" *) - | GApp (loc', f', args') -> GApp (join_loc loc' loc, f',args'@args) + | GApp (loc', f', args') -> GApp (Loc.merge loc' loc, f',args'@args) | _ -> GApp (loc, c, args)) | CRecord (loc, _, fs) -> let cargs = @@ -1424,7 +1424,7 @@ let internalize sigma globalenv env allow_patvar lvar c = (tm,ind)::inds, Option.fold_right Idset.add extra_id ex_ids, List.rev_append match_td matchs) tms ([],Idset.empty,[]) in let env' = Idset.fold - (fun var bli -> push_name_env lvar (Variable,[],[],[]) bli (dummy_loc,Name var)) + (fun var bli -> push_name_env lvar (Variable,[],[],[]) bli (Loc.ghost,Name var)) (Idset.union ex_ids as_in_vars) (reset_hidden_inductive_implicit_test env) in (* PatVars before a real pattern do not need to be matched *) let stripped_match_from_in = let rec aux = function @@ -1436,12 +1436,12 @@ let internalize sigma globalenv env allow_patvar lvar c = | [] -> Option.map (intern_type env') rtnpo (* Only PatVar in "in" clauses *) | l -> let thevars,thepats=List.split l in Some ( - GCases(dummy_loc,Term.RegularStyle,Some (GSort (dummy_loc,GType None)), (* "return Type" *) - List.map (fun id -> GVar (dummy_loc,id),(Name id,None)) thevars, (* "match v1,..,vn" *) - [dummy_loc,[],thepats, (* "|p1,..,pn" *) - Option.cata (intern_type env') (GHole(dummy_loc,Evar_kinds.CasesType)) rtnpo; (* "=> P" is there were a P "=> _" else *) - dummy_loc,[],list_make (List.length thepats) (PatVar(dummy_loc,Anonymous)), (* "|_,..,_" *) - GHole(dummy_loc,Evar_kinds.ImpossibleCase) (* "=> _" *)])) + GCases(Loc.ghost,Term.RegularStyle,Some (GSort (Loc.ghost,GType None)), (* "return Type" *) + List.map (fun id -> GVar (Loc.ghost,id),(Name id,None)) thevars, (* "match v1,..,vn" *) + [Loc.ghost,[],thepats, (* "|p1,..,pn" *) + Option.cata (intern_type env') (GHole(Loc.ghost,Evar_kinds.CasesType)) rtnpo; (* "=> P" is there were a P "=> _" else *) + Loc.ghost,[],list_make (List.length thepats) (PatVar(Loc.ghost,Anonymous)), (* "|_,..,_" *) + GHole(Loc.ghost,Evar_kinds.ImpossibleCase) (* "=> _" *)])) in let eqns' = List.map (intern_eqn (List.length tms) env) eqns in GCases (loc, sty, rtnpo, tms, List.flatten eqns') @@ -1451,7 +1451,7 @@ let internalize sigma globalenv env allow_patvar lvar c = let ((b',(na',_)),_,_) = intern_case_item env' Idset.empty (b,(na,None)) in let p' = Option.map (fun u -> let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env') - (dummy_loc,na') in + (Loc.ghost,na') in intern_type env'' u) po in GLetTuple (loc, List.map snd nal, (na', p'), b', intern (List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c) @@ -1460,7 +1460,7 @@ let internalize sigma globalenv env allow_patvar lvar c = let ((c',(na',_)),_,_) = intern_case_item env' Idset.empty (c,(na,None)) in (* no "in" no match to ad too *) let p' = Option.map (fun p -> let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env) - (dummy_loc,na') in + (Loc.ghost,na') in intern_type env'' p) po in GIf (loc, c', (na', p'), intern env b1, intern env b2) | CHole (loc, k) -> @@ -1516,7 +1516,7 @@ let internalize sigma globalenv env allow_patvar lvar c = let extra_id,na = match tm', na with | GVar (loc,id), None when Idset.mem id env.ids -> Some id,(loc,Name id) | GRef (loc, VarRef id), None -> Some id,(loc,Name id) - | _, None -> None,(dummy_loc,Anonymous) + | _, None -> None,(Loc.ghost,Anonymous) | _, Some (loc,na) -> None,(loc,na) in (* the "in" part *) let match_td,typ = match t with @@ -1540,7 +1540,7 @@ let internalize sigma globalenv env allow_patvar lvar c = match case_rel_ctxt,arg_pats with (* LetIn in the rel_context *) |(_,Some _,_)::t, l when not with_letin -> - canonize_args t l forbidden_names match_acc ((dummy_loc,Anonymous)::var_acc) + canonize_args t l forbidden_names match_acc ((Loc.ghost,Anonymous)::var_acc) |[],[] -> (add_name match_acc na, var_acc) |_::t,PatVar (loc,x)::tt -> diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 6f01bb466..39c307bcb 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -76,7 +76,7 @@ let check_required_library d = (* Loading silently ... let m, prefix = list_sep_last d' in read_library - (dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m) + (Loc.ghost,make_qualid (make_dirpath (List.rev prefix)) m) *) (* or failing ...*) error ("Library "^(string_of_dirpath dir)^" has to be required first.") diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 9fde5e219..e56d3b9ae 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -119,7 +119,7 @@ let remove_sections dir = dir let interval loc = - let loc1,loc2 = Pp.unloc loc in + let loc1,loc2 = Loc.unloc loc in loc1, loc2-1 let dump_ref loc filepath modpath ident ty = @@ -138,7 +138,7 @@ let add_glob_gen loc sp lib_dp ty = dump_ref loc filepath modpath ident ty let add_glob loc ref = - if dump () && loc <> Pp.dummy_loc then + if dump () && loc <> Loc.ghost then let sp = Nametab.path_of_global ref in let lib_dp = Lib.library_part ref in let ty = type_of_global_ref ref in @@ -149,7 +149,7 @@ let mp_of_kn kn = Names.MPdot (mp,l) let add_glob_kn loc kn = - if dump () && loc <> Pp.dummy_loc then + if dump () && loc <> Loc.ghost then let sp = Nametab.path_of_syndef kn in let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in add_glob_gen loc sp lib_dp "syndef" @@ -232,7 +232,7 @@ let cook_notation df sc = let dump_notation (loc,(df,_)) sc sec = (* We dump the location of the opening '"' *) - dump_string (Printf.sprintf "not %d %s %s\n" (fst (Pp.unloc loc)) + dump_string (Printf.sprintf "not %d %s %s\n" (fst (Loc.unloc loc)) (Names.string_of_dirpath (Lib.current_dirpath sec)) (cook_notation df sc)) let dump_notation_location posl df (((path,secpath),_),sc) = diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 469df1222..73354fa40 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -22,19 +22,19 @@ val dump_to_dotglob : unit -> unit val pause : unit -> unit val continue : unit -> unit -val add_glob : Pp.loc -> Globnames.global_reference -> unit -val add_glob_kn : Pp.loc -> Names.kernel_name -> unit - -val dump_definition : Pp.loc * Names.identifier -> bool -> string -> unit -val dump_moddef : Pp.loc -> Names.module_path -> string -> unit -val dump_modref : Pp.loc -> Names.module_path -> string -> unit -val dump_reference : Pp.loc -> string -> string -> string -> unit -val dump_libref : Pp.loc -> Names.dir_path -> string -> unit +val add_glob : Loc.t -> Globnames.global_reference -> unit +val add_glob_kn : Loc.t -> Names.kernel_name -> unit + +val dump_definition : Loc.t * Names.identifier -> bool -> string -> unit +val dump_moddef : Loc.t -> Names.module_path -> string -> unit +val dump_modref : Loc.t -> Names.module_path -> string -> unit +val dump_reference : Loc.t -> string -> string -> string -> unit +val dump_libref : Loc.t -> Names.dir_path -> string -> unit val dump_notation_location : (int * int) list -> Constrexpr.notation -> (Notation.notation_location * Notation_term.scope_name option) -> unit -val dump_binding : Pp.loc -> Names.Idset.elt -> unit +val dump_binding : Loc.t -> Names.Idset.elt -> unit val dump_notation : - Pp.loc * (Constrexpr.notation * Notation.notation_location) -> + Loc.t * (Constrexpr.notation * Notation.notation_location) -> Notation_term.scope_name option -> bool -> unit val dump_constraint : Constrexpr.typeclass_constraint -> bool -> string -> unit diff --git a/interp/genarg.mli b/interp/genarg.mli index 2bd19632e..51266b5eb 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Loc open Pp open Names open Term @@ -19,7 +20,7 @@ open Term open Evd open Misctypes -val loc_of_or_by_notation : ('a -> loc) -> 'a or_by_notation -> loc +val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t (** In globalize tactics, we need to keep the initial [constr_expr] to recompute in the environment by the effective calls to Intro, Inversion, etc diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 9389a1690..69f70deef 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -60,7 +60,7 @@ let cache_generalizable_type (_,(local,cmd)) = let load_generalizable_type _ (_,(local,cmd)) = generalizable_table := add_generalizable cmd !generalizable_table -let in_generalizable : bool * identifier located list option -> obj = +let in_generalizable : bool * identifier Loc.located list option -> obj = declare_object {(default_object "GENERALIZED-IDENT") with load_function = load_generalizable_type; cache_function = cache_generalizable_type; @@ -253,7 +253,7 @@ let combine_params avoid fn applied needed = let combine_params_freevar = fun avoid (_, (na, _, _)) -> let id' = next_name_away_from na avoid in - (CRef (Ident (dummy_loc, id')), Idset.add id' avoid) + (CRef (Ident (Loc.ghost, id')), Idset.add id' avoid) let destClassApp cl = match cl with diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 6297a17d2..5aa77f708 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Loc open Names open Decl_kinds open Term @@ -24,8 +25,8 @@ open Typeclasses val declare_generalizable : Vernacexpr.locality_flag -> (identifier located) list option -> unit val ids_of_list : identifier list -> Idset.t -val destClassApp : constr_expr -> loc * reference * constr_expr list -val destClassAppExpl : constr_expr -> loc * reference * (constr_expr * explicitation located option) list +val destClassApp : constr_expr -> Loc.t * reference * constr_expr list +val destClassAppExpl : constr_expr -> Loc.t * reference * (constr_expr * explicitation located option) list (** Fragile, should be used only for construction a set of identifiers to avoid *) @@ -39,7 +40,7 @@ val free_vars_of_binders : order with the location of their first occurence *) val generalizable_vars_of_glob_constr : ?bound:Idset.t -> ?allowed:Idset.t -> - glob_constr -> (Names.identifier * loc) list + glob_constr -> (Names.identifier * Loc.t) list val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier diff --git a/interp/modintern.ml b/interp/modintern.ml index 18d3a9c1c..d3468c463 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -46,19 +46,19 @@ let error_result_must_be_signature () = error "The result module type must be a signature." let error_not_a_modtype_loc loc s = - Compat.Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModuleType s)) + Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModuleType s)) let error_not_a_module_loc loc s = - Compat.Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModule s)) + Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModule s)) let error_not_a_module_nor_modtype_loc loc s = - Compat.Loc.raise loc (ModuleInternalizationError (NotAModuleNorModtype s)) + Loc.raise loc (ModuleInternalizationError (NotAModuleNorModtype s)) let error_incorrect_with_in_module loc = - Compat.Loc.raise loc (ModuleInternalizationError IncorrectWithInModule) + Loc.raise loc (ModuleInternalizationError IncorrectWithInModule) let error_application_to_module_type loc = - Compat.Loc.raise loc (ModuleInternalizationError IncorrectModuleApplication) + Loc.raise loc (ModuleInternalizationError IncorrectModuleApplication) @@ -149,7 +149,7 @@ let loc_of_module = function let check_module_argument_is_path me' = function | CMident _ -> () | (CMapply (loc,_,_) | CMwith (loc,_,_)) -> - Compat.Loc.raise loc + Loc.raise loc (Modops.ModuleTypingError (Modops.ApplicationToNotPath me')) let rec interp_modexpr env = function diff --git a/interp/modintern.mli b/interp/modintern.mli index 860f66790..fc3617ce2 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Loc open Declarations open Environ open Entries diff --git a/interp/notation.ml b/interp/notation.ml index a76ede48c..e42bd787c 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -219,7 +219,7 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) type required_module = full_path * string list type 'a prim_token_interpreter = - loc -> 'a -> glob_constr + Loc.t -> 'a -> glob_constr type cases_pattern_status = bool (* true = use prim token in patterns *) @@ -227,7 +227,7 @@ type 'a prim_token_uninterpreter = glob_constr list * (glob_constr -> 'a option) * cases_pattern_status type internal_prim_token_interpreter = - loc -> prim_token -> required_module * (unit -> glob_constr) + Loc.t -> prim_token -> required_module * (unit -> glob_constr) let prim_token_interpreter_tab = (Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t) @@ -416,8 +416,8 @@ let uninterp_prim_token_ind_pattern ind args = if not b then raise Notation_ops.No_match; let args' = List.map (fun x -> snd (glob_constr_of_closed_cases_pattern x)) args in - let ref = GRef (dummy_loc,ref) in - match numpr (GApp (dummy_loc,ref,args')) with + let ref = GRef (Loc.ghost,ref) in + match numpr (GApp (Loc.ghost,ref,args')) with | None -> raise Notation_ops.No_match | Some n -> (sc,n) with Not_found -> raise Notation_ops.No_match @@ -435,7 +435,7 @@ let uninterp_prim_token_cases_pattern c = let availability_of_prim_token n printer_scope local_scopes = let f scope = - try ignore (Hashtbl.find prim_token_interpreter_tab scope dummy_loc n); true + try ignore (Hashtbl.find prim_token_interpreter_tab scope Loc.ghost n); true with Not_found -> false in let scopes = make_current_scopes local_scopes in Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes) @@ -654,7 +654,7 @@ let pr_scope_classes sc = let pr_notation_info prglob ntn c = str "\"" ++ str ntn ++ str "\" := " ++ - prglob (Notation_ops.glob_constr_of_notation_constr dummy_loc c) + prglob (Notation_ops.glob_constr_of_notation_constr Loc.ghost c) let pr_named_scope prglob scope sc = (if scope = default_scope then @@ -727,7 +727,7 @@ let error_notation_not_reference loc ntn = let interp_notation_as_global_reference loc test ntn sc = let scopes = match sc with | Some sc -> - Gmap.add sc (find_scope (find_delimiters_scope dummy_loc sc)) Gmap.empty + Gmap.add sc (find_scope (find_delimiters_scope Loc.ghost sc)) Gmap.empty | None -> !scope_map in let ntns = browse_notation true ntn scopes in let refs = List.map (global_reference_of_notation test) ntns in diff --git a/interp/notation.mli b/interp/notation.mli index 3f66f993a..d1446527f 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -54,7 +54,7 @@ val find_scope : scope_name -> scope (** Declare delimiters for printing *) val declare_delimiters : scope_name -> delimiters -> unit -val find_delimiters_scope : loc -> delimiters -> scope_name +val find_delimiters_scope : Loc.t -> delimiters -> scope_name (** {6 Declare and uses back and forth an interpretation of primitive token } *) @@ -68,7 +68,7 @@ type required_module = full_path * string list type cases_pattern_status = bool (** true = use prim token in patterns *) type 'a prim_token_interpreter = - loc -> 'a -> glob_constr + Loc.t -> 'a -> glob_constr type 'a prim_token_uninterpreter = glob_constr list * (glob_constr -> 'a option) * cases_pattern_status @@ -82,9 +82,9 @@ val declare_string_interpreter : scope_name -> required_module -> (** Return the [term]/[cases_pattern] bound to a primitive token in a given scope context*) -val interp_prim_token : loc -> prim_token -> local_scopes -> +val interp_prim_token : Loc.t -> prim_token -> local_scopes -> glob_constr * (notation_location * scope_name option) -val interp_prim_token_cases_pattern_expr : loc -> (global_reference -> unit) -> prim_token -> +val interp_prim_token_cases_pattern_expr : Loc.t -> (global_reference -> unit) -> prim_token -> local_scopes -> raw_cases_pattern_expr * (notation_location * scope_name option) (** Return the primitive token associated to a [term]/[cases_pattern]; @@ -113,7 +113,7 @@ val declare_notation_interpretation : notation -> scope_name option -> val declare_uninterpretation : interp_rule -> interpretation -> unit (** Return the interpretation bound to a notation *) -val interp_notation : loc -> notation -> local_scopes -> +val interp_notation : Loc.t -> notation -> local_scopes -> interpretation * (notation_location * scope_name option) (** Return the possible notations for a given term *) @@ -137,7 +137,7 @@ val level_of_notation : notation -> level (** raise [Not_found] if no level *) (** {6 Miscellaneous} *) -val interp_notation_as_global_reference : loc -> (global_reference -> bool) -> +val interp_notation_as_global_reference : Loc.t -> (global_reference -> bool) -> notation -> delimiters option -> global_reference (** Checks for already existing notations *) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index b1067fa47..857e827a9 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -165,7 +165,7 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with let rec eq_glob_constr t1 t2 = compare_glob_constr eq_glob_constr (fun _ -> ()) t1 t2 -let subtract_loc loc1 loc2 = make_loc (fst (unloc loc1),fst (unloc loc2)-1) +let subtract_loc loc1 loc2 = Loc.make_loc (fst (Loc.unloc loc1),fst (Loc.unloc loc2)-1) let check_is_hole id = function GHole _ -> () | t -> user_err_loc (loc_of_glob_constr t,"", @@ -209,7 +209,7 @@ let compare_recursive_parts found f (iterator,subc) = | Some (x,y,Some lassoc) -> let newfound = (pi1 !found, (x,y) :: pi2 !found, pi3 !found) in let iterator = - f (if lassoc then subst_glob_vars [y,GVar(dummy_loc,x)] iterator + f (if lassoc then subst_glob_vars [y,GVar(Loc.ghost,x)] iterator else iterator) in (* found have been collected by compare_constr *) found := newfound; @@ -467,7 +467,7 @@ let abstract_return_type_context pi mklam tml rtno = let abstract_return_type_context_glob_constr = abstract_return_type_context (fun (_,_,nal) -> nal) (fun na c -> - GLambda(dummy_loc,na,Explicit,GHole(dummy_loc,Evar_kinds.InternalHole),c)) + GLambda(Loc.ghost,na,Explicit,GHole(Loc.ghost,Evar_kinds.InternalHole),c)) let abstract_return_type_context_notation_constr = abstract_return_type_context snd @@ -513,8 +513,8 @@ let match_opt f sigma t1 t2 = match (t1,t2) with let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with | (_,Name id2) when List.mem id2 (fst metas) -> let rhs = match na1 with - | Name id1 -> GVar (dummy_loc,id1) - | Anonymous -> GHole (dummy_loc,Evar_kinds.InternalHole) in + | Name id1 -> GVar (Loc.ghost,id1) + | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole) in alp, bind_env alp sigma id2 rhs | (Name id1,Name id2) -> (id1,id2)::alp,sigma | (Anonymous,Anonymous) -> alp,sigma @@ -689,8 +689,8 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = | b1, NLambda (Name id,NHole _,b2) when inner -> let id' = Namegen.next_ident_away id (free_glob_vars b1) in match_in u alp metas (bind_binder sigma id - [(Name id',Explicit,None,GHole(dummy_loc,Evar_kinds.BinderType (Name id')))]) - (mkGApp dummy_loc b1 (GVar (dummy_loc,id'))) b2 + [(Name id',Explicit,None,GHole(Loc.ghost,Evar_kinds.BinderType (Name id')))]) + (mkGApp Loc.ghost b1 (GVar (Loc.ghost,id'))) b2 | (GRec _ | GEvar _), _ | _,_ -> raise No_match @@ -721,7 +721,7 @@ let match_notation_constr u c (metas,pat) = with Not_found -> (* Happens for binders bound to Anonymous *) (* Find a better way to propagate Anonymous... *) - GVar (dummy_loc,x) in + GVar (Loc.ghost,x) in List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') -> match typ with | NtnTypeConstr -> @@ -736,7 +736,7 @@ let match_notation_constr u c (metas,pat) = let add_patterns_for_params ind l = let mib,_ = Global.lookup_inductive ind in let nparams = mib.Declarations.mind_nparams in - Util.list_addn nparams (PatVar (dummy_loc,Anonymous)) l + Util.list_addn nparams (PatVar (Loc.ghost,Anonymous)) l let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v = try diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index dee1203b3..ef92500f1 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -28,12 +28,12 @@ val eq_glob_constr : glob_constr -> glob_constr -> bool (** Re-interpret a notation as a [glob_constr], taking care of binders *) -val glob_constr_of_notation_constr_with_binders : Pp.loc -> +val glob_constr_of_notation_constr_with_binders : Loc.t -> ('a -> name -> 'a * name) -> ('a -> notation_constr -> glob_constr) -> 'a -> notation_constr -> glob_constr -val glob_constr_of_notation_constr : Pp.loc -> notation_constr -> glob_constr +val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr (** [match_notation_constr] matches a [glob_constr] against a notation interpretation; raise [No_match] if the matching fails *) diff --git a/interp/reserve.ml b/interp/reserve.ml index f170ff023..a72b10ad6 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -95,7 +95,7 @@ let anonymize_if_reserved na t = match na with (try Notation_ops.notation_constr_of_glob_constr [] [] t = find_reserved_type id with UserError _ -> false) - then GHole (dummy_loc,Evar_kinds.BinderType na) + then GHole (Loc.ghost,Evar_kinds.BinderType na) else t with Not_found -> t) | Anonymous -> t diff --git a/interp/reserve.mli b/interp/reserve.mli index d52460b08..d23bb8789 100644 --- a/interp/reserve.mli +++ b/interp/reserve.mli @@ -6,11 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Loc open Pp open Names open Glob_term open Notation_term val declare_reserved_type : identifier located list -> notation_constr -> unit -val find_reserved_type : identifier ->notation_constr +val find_reserved_type : identifier -> notation_constr val anonymize_if_reserved : name -> glob_constr -> glob_constr diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli index eaa4863c6..be9feead3 100644 --- a/interp/smartlocate.mli +++ b/interp/smartlocate.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Loc open Pp open Names open Libnames diff --git a/interp/topconstr.ml b/interp/topconstr.ml index bc9d3b851..8ec834d76 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -59,7 +59,7 @@ let ids_of_cases_tomatch tms = List.fold_right (fun (_,(ona,indnal)) l -> Option.fold_right (fun t -> (@) (ids_of_cases_indtype t)) - indnal (Option.fold_right (down_located name_cons) ona l)) + indnal (Option.fold_right (Loc.down_located name_cons) ona l)) tms [] let is_constructor id = @@ -84,7 +84,7 @@ let rec cases_pattern_fold_names f a = function let ids_of_pattern_list = List.fold_left - (located_fold_left + (Loc.located_fold_left (List.fold_left (cases_pattern_fold_names Idset.add))) Idset.empty @@ -117,7 +117,7 @@ let fold_constr_expr_with_binders g f n acc = function (* The following is an approximation: we don't know exactly if an ident is binding nor to which subterms bindings apply *) let acc = List.fold_left (f n) acc (l@List.flatten ll) in - List.fold_left (fun acc bl -> fold_local_binders g f n acc (CHole (dummy_loc,None)) bl) acc bll + List.fold_left (fun acc bl -> fold_local_binders g f n acc (CHole (Loc.ghost,None)) bl) acc bll | CGeneralization (_,_,_,c) -> f n acc c | CDelimiters (loc,_,a) -> f n acc a | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ -> @@ -131,12 +131,12 @@ let fold_constr_expr_with_binders g f n acc = function let ids = ids_of_pattern_list patl in f (Idset.fold g ids n) acc rhs) bl acc | CLetTuple (loc,nal,(ona,po),b,c) -> - let n' = List.fold_right (down_located (name_fold g)) nal n in - f (Option.fold_right (down_located (name_fold g)) ona n') (f n acc b) c + let n' = List.fold_right (Loc.down_located (name_fold g)) nal n in + f (Option.fold_right (Loc.down_located (name_fold g)) ona n') (f n acc b) c | CIf (_,c,(ona,po),b1,b2) -> let acc = f n (f n (f n acc b1) b2) c in Option.fold_left - (f (Option.fold_right (down_located (name_fold g)) ona n)) acc po + (f (Option.fold_right (Loc.down_located (name_fold g)) ona n)) acc po | CFix (loc,_,l) -> let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in List.fold_right (fun (_,(_,o),lb,t,c) acc -> @@ -177,7 +177,7 @@ let split_at_annot bl na = (* Used in correctness and interface *) -let map_binder g e nal = List.fold_right (down_located (name_fold g)) nal e +let map_binder g e nal = List.fold_right (Loc.down_located (name_fold g)) nal e let map_binders f g e bl = (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) @@ -221,11 +221,11 @@ let map_constr_expr_with_binders g f e = function let po = Option.map (f (List.fold_right g ids e)) rtnpo in CCases (loc, sty, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl) | CLetTuple (loc,nal,(ona,po),b,c) -> - let e' = List.fold_right (down_located (name_fold g)) nal e in - let e'' = Option.fold_right (down_located (name_fold g)) ona e in + let e' = List.fold_right (Loc.down_located (name_fold g)) nal e in + let e'' = Option.fold_right (Loc.down_located (name_fold g)) ona e in CLetTuple (loc,nal,(ona,Option.map (f e'') po),f e b,f e' c) | CIf (loc,c,(ona,po),b1,b2) -> - let e' = Option.fold_right (down_located (name_fold g)) ona e in + let e' = Option.fold_right (Loc.down_located (name_fold g)) ona e in CIf (loc,f e c,(ona,Option.map (f e') po),f e b1,f e b2) | CFix (loc,id,dl) -> CFix (loc,id,List.map (fun (id,n,bl,t,d) -> @@ -254,20 +254,20 @@ let rec replace_vars_constr_expr l = function (* Concrete syntax for modules and modules types *) type with_declaration_ast = - | CWith_Module of identifier list located * qualid located - | CWith_Definition of identifier list located * constr_expr + | CWith_Module of identifier list Loc.located * qualid Loc.located + | CWith_Definition of identifier list Loc.located * constr_expr type module_ast = - | CMident of qualid located - | CMapply of loc * module_ast * module_ast - | CMwith of loc * module_ast * with_declaration_ast + | CMident of qualid Loc.located + | CMapply of Loc.t * module_ast * module_ast + | CMwith of Loc.t * module_ast * with_declaration_ast (* Returns the ranges of locs of the notation that are not occupied by args *) (* and which are then occupied by proper symbols of the notation (or spaces) *) let locs_of_notation loc locs ntn = - let (bl,el) = unloc loc in - let locs = List.map unloc locs in + let (bl, el) = Loc.unloc loc in + let locs = List.map Loc.unloc locs in let rec aux pos = function | [] -> if pos = el then [] else [(pos,el-1)] | (ba,ea)::l ->if pos = ba then aux ea l else (pos,ba-1)::aux ea l diff --git a/interp/topconstr.mli b/interp/topconstr.mli index bd9e776c9..d99846d12 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Loc open Pp open Names open Libnames @@ -47,10 +48,10 @@ val map_constr_expr_with_binders : 'a -> constr_expr -> constr_expr val ntn_loc : - loc -> constr_notation_substitution -> string -> (int * int) list + Loc.t -> constr_notation_substitution -> string -> (int * int) list val patntn_loc : - loc -> cases_pattern_notation_substitution -> string -> (int * int) list + Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list (** For cases pattern parsing errors *) -val error_invalid_pattern_notation : Pp.loc -> 'a +val error_invalid_pattern_notation : Loc.t -> 'a diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 605be512c..d8387b9df 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Loc open Pp open Names open Libnames @@ -36,27 +37,27 @@ type proj_flag = int option (** [Some n] = proj of the n-th visible argument *) type prim_token = Numeral of Bigint.bigint | String of string type raw_cases_pattern_expr = - | RCPatAlias of loc * raw_cases_pattern_expr * identifier - | RCPatCstr of loc * Globnames.global_reference + | RCPatAlias of Loc.t * raw_cases_pattern_expr * identifier + | RCPatCstr of Loc.t * Globnames.global_reference * raw_cases_pattern_expr list * raw_cases_pattern_expr list (** [CPatCstr (_, Inl c, l1, l2)] represents (@c l1) l2 *) - | RCPatAtom of loc * identifier option - | RCPatOr of loc * raw_cases_pattern_expr list + | RCPatAtom of Loc.t * identifier option + | RCPatOr of Loc.t * raw_cases_pattern_expr list type cases_pattern_expr = - | CPatAlias of loc * cases_pattern_expr * identifier - | CPatCstr of loc * reference + | CPatAlias of Loc.t * cases_pattern_expr * identifier + | CPatCstr of Loc.t * reference * cases_pattern_expr list * cases_pattern_expr list (** [CPatCstr (_, Inl c, l1, l2)] represents (@c l1) l2 *) - | CPatAtom of loc * reference option - | CPatOr of loc * cases_pattern_expr list - | CPatNotation of loc * notation * cases_pattern_notation_substitution + | CPatAtom of Loc.t * reference option + | CPatOr of Loc.t * cases_pattern_expr list + | CPatNotation of Loc.t * notation * cases_pattern_notation_substitution * cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents (notation n applied with substitution l1) applied to arguments l2 *) - | CPatPrim of loc * prim_token - | CPatRecord of loc * (reference * cases_pattern_expr) list - | CPatDelimiters of loc * string * cases_pattern_expr + | CPatPrim of Loc.t * prim_token + | CPatRecord of Loc.t * (reference * cases_pattern_expr) list + | CPatDelimiters of Loc.t * string * cases_pattern_expr and cases_pattern_notation_substitution = cases_pattern_expr list * (** for constr subterms *) @@ -64,31 +65,31 @@ and cases_pattern_notation_substitution = type constr_expr = | CRef of reference - | CFix of loc * identifier located * fix_expr list - | CCoFix of loc * identifier located * cofix_expr list - | CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr - | CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr - | CLetIn of loc * name located * constr_expr * constr_expr - | CAppExpl of loc * (proj_flag * reference) * constr_expr list - | CApp of loc * (proj_flag * constr_expr) * + | CFix of Loc.t * identifier located * fix_expr list + | CCoFix of Loc.t * identifier located * cofix_expr list + | CProdN of Loc.t * (name located list * binder_kind * constr_expr) list * constr_expr + | CLambdaN of Loc.t * (name located list * binder_kind * constr_expr) list * constr_expr + | CLetIn of Loc.t * name located * constr_expr * constr_expr + | CAppExpl of Loc.t * (proj_flag * reference) * constr_expr list + | CApp of Loc.t * (proj_flag * constr_expr) * (constr_expr * explicitation located option) list - | CRecord of loc * constr_expr option * (reference * constr_expr) list - | CCases of loc * case_style * constr_expr option * + | CRecord of Loc.t * constr_expr option * (reference * constr_expr) list + | CCases of Loc.t * case_style * constr_expr option * (constr_expr * (name located option * cases_pattern_expr option)) list * - (loc * cases_pattern_expr list located list * constr_expr) list - | CLetTuple of loc * name located list * (name located option * constr_expr option) * + (Loc.t * cases_pattern_expr list located list * constr_expr) list + | CLetTuple of Loc.t * name located list * (name located option * constr_expr option) * constr_expr * constr_expr - | CIf of loc * constr_expr * (name located option * constr_expr option) + | CIf of Loc.t * constr_expr * (name located option * constr_expr option) * constr_expr * constr_expr - | CHole of loc * Evar_kinds.t option - | CPatVar of loc * (bool * patvar) - | CEvar of loc * existential_key * constr_expr list option - | CSort of loc * glob_sort - | CCast of loc * constr_expr * constr_expr cast_type - | CNotation of loc * notation * constr_notation_substitution - | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr - | CPrim of loc * prim_token - | CDelimiters of loc * string * constr_expr + | CHole of Loc.t * Evar_kinds.t option + | CPatVar of Loc.t * (bool * patvar) + | CEvar of Loc.t * existential_key * constr_expr list option + | CSort of Loc.t * glob_sort + | CCast of Loc.t * constr_expr * constr_expr cast_type + | CNotation of Loc.t * notation * constr_notation_substitution + | CGeneralization of Loc.t * binding_kind * abstraction_kind option * constr_expr + | CPrim of Loc.t * prim_token + | CDelimiters of Loc.t * string * constr_expr and fix_expr = identifier located * (identifier located option * recursion_order_expr) * @@ -126,5 +127,5 @@ type with_declaration_ast = type module_ast = | CMident of qualid located - | CMapply of loc * module_ast * module_ast - | CMwith of loc * module_ast * with_declaration_ast + | CMapply of Loc.t * module_ast * module_ast + | CMwith of Loc.t * module_ast * with_declaration_ast diff --git a/intf/extend.mli b/intf/extend.mli index 6b29fc747..3b14ceea9 100644 --- a/intf/extend.mli +++ b/intf/extend.mli @@ -6,14 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Compat - (** Entry keys for constr notations *) type side = Left | Right type production_position = - | BorderProd of side * gram_assoc option + | BorderProd of side * Compat.gram_assoc option | InternalProd type production_level = diff --git a/intf/genredexpr.mli b/intf/genredexpr.mli index 8aab193fd..a7e08dbbc 100644 --- a/intf/genredexpr.mli +++ b/intf/genredexpr.mli @@ -44,5 +44,5 @@ type ('a,'b,'c) red_expr_gen = type ('a,'b,'c) may_eval = | ConstrTerm of 'a | ConstrEval of ('a,'b,'c) red_expr_gen * 'a - | ConstrContext of (Pp.loc * Names.identifier) * 'a + | ConstrContext of (Loc.t * Names.identifier) * 'a | ConstrTypeOf of 'a diff --git a/intf/glob_term.mli b/intf/glob_term.mli index 7ee0320f0..5cb369562 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -27,31 +27,31 @@ open Misctypes locs here refers to the ident's location, not whole pat *) type cases_pattern = - | PatVar of loc * name - | PatCstr of loc * constructor * cases_pattern list * name + | PatVar of Loc.t * name + | PatCstr of Loc.t * constructor * cases_pattern list * name (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *) type glob_constr = - | GRef of (loc * global_reference) - | GVar of (loc * identifier) - | GEvar of loc * existential_key * glob_constr list option - | GPatVar of loc * (bool * patvar) (** Used for patterns only *) - | GApp of loc * glob_constr * glob_constr list - | GLambda of loc * name * binding_kind * glob_constr * glob_constr - | GProd of loc * name * binding_kind * glob_constr * glob_constr - | GLetIn of loc * name * glob_constr * glob_constr - | GCases of loc * case_style * glob_constr option * tomatch_tuples * cases_clauses + | GRef of (Loc.t * global_reference) + | GVar of (Loc.t * identifier) + | GEvar of Loc.t * existential_key * glob_constr list option + | GPatVar of Loc.t * (bool * patvar) (** Used for patterns only *) + | GApp of Loc.t * glob_constr * glob_constr list + | GLambda of Loc.t * name * binding_kind * glob_constr * glob_constr + | GProd of Loc.t * name * binding_kind * glob_constr * glob_constr + | GLetIn of Loc.t * name * glob_constr * glob_constr + | GCases of Loc.t * case_style * glob_constr option * tomatch_tuples * cases_clauses (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *) - | GLetTuple of loc * name list * (name * glob_constr option) * + | GLetTuple of Loc.t * name list * (name * glob_constr option) * glob_constr * glob_constr - | GIf of loc * glob_constr * (name * glob_constr option) * glob_constr * glob_constr - | GRec of loc * fix_kind * identifier array * glob_decl list array * + | GIf of Loc.t * glob_constr * (name * glob_constr option) * glob_constr * glob_constr + | GRec of Loc.t * fix_kind * identifier array * glob_decl list array * glob_constr array * glob_constr array - | GSort of loc * glob_sort - | GHole of (loc * Evar_kinds.t) - | GCast of loc * glob_constr * glob_constr cast_type + | GSort of Loc.t * glob_sort + | GHole of (Loc.t * Evar_kinds.t) + | GCast of Loc.t * glob_constr * glob_constr cast_type and glob_decl = name * binding_kind * glob_constr option * glob_constr @@ -65,14 +65,14 @@ and fix_kind = | GCoFix of int and predicate_pattern = - name * (loc * inductive * name list) option + name * (Loc.t * inductive * name list) option (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)]. *) and tomatch_tuple = (glob_constr * predicate_pattern) and tomatch_tuples = tomatch_tuple list -and cases_clause = (loc * identifier list * cases_pattern list * glob_constr) +and cases_clause = (Loc.t * identifier list * cases_pattern list * glob_constr) (** [(p,il,cl,t)] = "|'cl' as 'il' => 't'" *) and cases_clauses = cases_clause list diff --git a/intf/misctypes.mli b/intf/misctypes.mli index a51145812..b9f5a6dbe 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -25,7 +25,7 @@ type intro_pattern_expr = | IntroFresh of identifier | IntroForthcoming of bool | IntroAnonymous -and or_and_intro_pattern_expr = (Pp.loc * intro_pattern_expr) list list +and or_and_intro_pattern_expr = (Loc.t * intro_pattern_expr) list list (** Move destination for hypothesis *) @@ -52,7 +52,7 @@ type 'a cast_type = type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier -type 'a explicit_bindings = (Pp.loc * quantified_hypothesis * 'a) list +type 'a explicit_bindings = (Loc.t * quantified_hypothesis * 'a) list type 'a bindings = | ImplicitBindings of 'a list @@ -66,13 +66,13 @@ type 'a with_bindings = 'a * 'a bindings type 'a or_var = | ArgArg of 'a - | ArgVar of Names.identifier Pp.located + | ArgVar of Names.identifier Loc.located -type 'a and_short_name = 'a * identifier Pp.located option +type 'a and_short_name = 'a * identifier Loc.located option type 'a or_by_notation = | AN of 'a - | ByNotation of (Pp.loc * string * string option) + | ByNotation of (Loc.t * string * string option) (* NB: the last string in [ByNotation] is actually a [Notation.delimiters], but this formulation avoids a useless dependency. *) diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 895eca2d9..ccf682a48 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Loc open Names open Constrexpr open Libnames @@ -19,7 +20,7 @@ open Misctypes open Locus open Pp -type 'a or_metaid = AI of 'a | MetaId of loc * string +type 'a or_metaid = AI of 'a | MetaId of Loc.t * string type direction_flag = bool (* true = Left-to-right false = right-to-right *) type lazy_flag = bool (* true = lazy false = eager *) @@ -154,15 +155,15 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr = | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis (* For ML extensions *) - | TacExtend of loc * string * 'lev generic_argument list + | TacExtend of Loc.t * string * 'lev generic_argument list (* For syntax extensions *) - | TacAlias of loc * string * + | TacAlias of Loc.t * string * (identifier * 'lev generic_argument) list * (dir_path * glob_tactic_expr) and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr = - | TacAtom of loc * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr + | TacAtom of Loc.t * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr | TacThen of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr array * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * @@ -193,16 +194,16 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_fun_ast = (* These are the possible arguments of a tactic definition *) and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg = - | TacDynamic of loc * Dyn.t + | TacDynamic of Loc.t * Dyn.t | TacVoid - | MetaIdArg of loc * bool * string + | MetaIdArg of Loc.t * bool * string | ConstrMayEval of ('constr,'cst,'pat) may_eval | IntroPattern of intro_pattern_expr located | Reference of 'ref | Integer of int - | TacCall of loc * + | TacCall of Loc.t * 'ref * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg list - | TacExternal of loc * string * string * + | TacExternal of Loc.t * string * string * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg list | TacFreshId of string or_var list | Tacexp of 'tac diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 3223e80b8..568d8a38e 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Loc open Pp open Names open Tacexpr @@ -175,7 +176,7 @@ type module_binder = bool option * lident list * module_ast_inl type grammar_tactic_prod_item_expr = | TacTerm of string - | TacNonTerm of loc * string * (Names.identifier * string) option + | TacNonTerm of Loc.t * string * (Names.identifier * string) option type syntax_modifier = | SetItemLevel of string list * Extend.production_level @@ -307,7 +308,7 @@ type vernac_expr = | VernacDeclareImplicits of locality_flag * reference or_by_notation * (explicitation * bool * bool) list list | VernacArguments of locality_flag * reference or_by_notation * - ((name * bool * (loc * string) option * bool * bool) list) list * + ((name * bool * (Loc.t * string) option * bool * bool) list) list * int * [ `SimplDontExposeCase | `SimplNeverUnfold | `Rename | `ExtraScopes | `ClearImplicits | `ClearScopes | `DefaultImplicits ] list | VernacArgumentsScope of locality_flag * reference or_by_notation * @@ -355,4 +356,4 @@ type vernac_expr = (* For extension *) | VernacExtend of string * raw_generic_argument list -and located_vernac_expr = loc * vernac_expr +and located_vernac_expr = Loc.t * vernac_expr diff --git a/lib/errors.ml b/lib/errors.ml index 026198a98..77f03f045 100644 --- a/lib/errors.ml +++ b/lib/errors.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -open Compat open Pp (* Errors *) @@ -32,7 +31,7 @@ let invalid_arg_loc (loc,s) = Loc.raise loc (Invalid_argument s) (* Like Exc_located, but specifies the outermost file read, the filename associated to the location of the error, and the error itself. *) -exception Error_in_file of string * (bool * string * loc) * exn +exception Error_in_file of string * (bool * string * Loc.t) * exn exception Timeout exception Drop diff --git a/lib/errors.mli b/lib/errors.mli index d04ebb3fe..3dd470a06 100644 --- a/lib/errors.mli +++ b/lib/errors.mli @@ -19,17 +19,17 @@ open Pp exception Anomaly of string * std_ppcmds val anomaly : string -> 'a val anomalylabstrm : string -> std_ppcmds -> 'a -val anomaly_loc : loc * string * std_ppcmds -> 'a +val anomaly_loc : Loc.t * string * std_ppcmds -> 'a exception UserError of string * std_ppcmds val error : string -> 'a val errorlabstrm : string -> std_ppcmds -> 'a -val user_err_loc : loc * string * std_ppcmds -> 'a +val user_err_loc : Loc.t * string * std_ppcmds -> 'a exception AlreadyDeclared of std_ppcmds val alreadydeclared : std_ppcmds -> 'a -val invalid_arg_loc : loc * string -> 'a +val invalid_arg_loc : Loc.t * string -> 'a (** [todo] is for running of an incomplete code its implementation is "do nothing" (or print a message), but this function should not be @@ -45,7 +45,7 @@ exception Quit input buffer associated to the location of the error (or the module name if boolean is true), and the error itself. *) -exception Error_in_file of string * (bool * string * loc) * exn +exception Error_in_file of string * (bool * string * Loc.t) * exn (** [register_handler h] registers [h] as a handler. When an expression is printed with [print e], it diff --git a/lib/lib.mllib b/lib/lib.mllib index 1cbf0c780..93fb748ac 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -3,6 +3,7 @@ Xml_parser Pp_control Compat Pp +Loc Errors Bigint Hashcons diff --git a/lib/loc.ml b/lib/loc.ml new file mode 100644 index 000000000..b2d83a78b --- /dev/null +++ b/lib/loc.ml @@ -0,0 +1,29 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp + +include Compat.Loc + +(* Locations management *) + +let dummy_loc = Compat.Loc.ghost +let join_loc = Compat.Loc.merge +let make_loc = Compat.make_loc +let unloc = Compat.unloc + +type 'a located = t * 'a +let located_fold_left f x (_,a) = f x a +let located_iter2 f (_,a) (_,b) = f a b +let down_located f (_,a) = f a + +let pr_located pr (loc, x) = + if Flags.do_beautify () && loc <> dummy_loc then + let (b, e) = unloc loc in + Pp.comment b ++ pr x ++ Pp.comment e + else pr x diff --git a/lib/loc.mli b/lib/loc.mli new file mode 100644 index 000000000..c8e0901e9 --- /dev/null +++ b/lib/loc.mli @@ -0,0 +1,44 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** {5 Basic types} *) + +type t = Compat.Loc.t + +exception Exc_located of t * exn + +type 'a located = t * 'a + +(** {5 Location manipulation} *) + +(** This is inherited from CAMPL4/5. *) + +val unloc : t -> int * int +val make_loc : int * int -> t +val ghost : t +val merge : t -> t -> t +val raise : t -> exn -> 'a + +(** {5 Location utilities} *) + +val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a +val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit + +val down_located : ('a -> 'b) -> 'a located -> 'b +(** Projects out a located object *) + +val pr_located : ('a -> Pp.std_ppcmds) -> 'a located -> Pp.std_ppcmds +(** Prints an object surrounded by its commented location *) + +(** {5 Backward compatibility} *) + +val dummy_loc : t +(** Same as [ghost] *) + +val join_loc : t -> t -> t +(** Same as [merge] *) diff --git a/lib/pp.ml4 b/lib/pp.ml4 index 789de8160..fb85af0eb 100644 --- a/lib/pp.ml4 +++ b/lib/pp.ml4 @@ -7,7 +7,6 @@ (************************************************************************) open Pp_control -open Compat (* This should not be used outside of this file. Use Flags.print_emacs instead. This one is updated when reading @@ -374,19 +373,6 @@ let string_of_ppcmds c = msg_with Format.str_formatter c; Format.flush_str_formatter () -(* Locations management *) -type loc = Loc.t -let dummy_loc = Loc.ghost -let join_loc = Loc.merge -let make_loc = make_loc -let unloc = unloc - -type 'a located = loc * 'a -let located_fold_left f x (_,a) = f x a -let located_iter2 f (_,a) (_,b) = f a b -let down_located f (_,a) = f a - - (* Copy paste from Util *) let pr_comma () = str "," ++ spc () @@ -467,10 +453,4 @@ let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v let prvect elem v = prvect_with_sep mt elem v -let pr_located pr (loc,x) = - if Flags.do_beautify() && loc<>dummy_loc then - let (b,e) = unloc loc in - comment b ++ pr x ++ comment e - else pr x - let surround p = hov 1 (str"(" ++ p ++ str")") diff --git a/lib/pp.mli b/lib/pp.mli index 09efc57a1..a1be529a9 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -7,7 +7,6 @@ (************************************************************************) open Pp_control -open Compat (** Modify pretty printing functions behavior for emacs ouput (special chars inserted at some places). This function should called once in @@ -125,19 +124,6 @@ val msgerr : std_ppcmds -> unit val msgerrnl : std_ppcmds -> unit val message : string -> unit (** = pPNL *) -(** {6 Location management. } *) - -type loc = Loc.t -val unloc : loc -> int * int -val make_loc : int * int -> loc -val dummy_loc : loc -val join_loc : loc -> loc -> loc - -type 'a located = loc * 'a -val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a -val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit -val down_located : ('a -> 'b) -> 'a located -> 'b - (** {6 Util copy/paste. } *) val pr_comma : unit -> std_ppcmds @@ -163,7 +149,6 @@ val prvecti_with_sep : (unit -> std_ppcmds) -> (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds val pr_enum : ('a -> std_ppcmds) -> 'a list -> std_ppcmds -val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds val pr_sequence : ('a -> std_ppcmds) -> 'a list -> std_ppcmds val surround : std_ppcmds -> std_ppcmds diff --git a/library/declaremods.mli b/library/declaremods.mli index 800e2eaa8..3064564ca 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Loc open Pp open Names open Entries diff --git a/library/lib.mli b/library/lib.mli index 318997067..382637e9e 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -161,7 +161,7 @@ val first_command_label : int val reset_label : int -> unit (** search the label registered immediately before adding some definition *) -val label_before_name : Names.identifier Pp.located -> int +val label_before_name : Names.identifier Loc.located -> int (** {6 We can get and set the state of the operations (used in [States]). } *) diff --git a/library/libnames.ml b/library/libnames.ml index 37ae97ace..f3e8d17f3 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -153,8 +153,8 @@ type global_dir_reference = (* this won't last long I hope! *) type reference = - | Qualid of qualid located - | Ident of identifier located + | Qualid of qualid Loc.located + | Ident of identifier Loc.located let qualid_of_reference = function | Qualid (loc,qid) -> loc, qid diff --git a/library/libnames.mli b/library/libnames.mli index 24bdd2048..227d1f3df 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Loc open Names (** {6 Dirpaths } *) @@ -109,7 +110,7 @@ type reference = val qualid_of_reference : reference -> qualid located val string_of_reference : reference -> string val pr_reference : reference -> std_ppcmds -val loc_of_reference : reference -> loc +val loc_of_reference : reference -> Loc.t (** Deprecated synonyms *) diff --git a/library/library.mli b/library/library.mli index 766e22afa..a19149332 100644 --- a/library/library.mli +++ b/library/library.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Loc open Pp open Names open Libnames diff --git a/library/nametab.ml b/library/nametab.ml index 2bdd71cc4..84f6c6542 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -8,7 +8,6 @@ open Errors open Util -open Compat open Pp open Names open Libnames diff --git a/library/nametab.mli b/library/nametab.mli index 871ed6676..b82ad0175 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -61,9 +61,9 @@ exception GlobalizationError of qualid exception GlobalizationConstantError of qualid (** Raises a globalization error *) -val error_global_not_found_loc : loc -> qualid -> 'a +val error_global_not_found_loc : Loc.t -> qualid -> 'a val error_global_not_found : qualid -> 'a -val error_global_constant_not_found_loc : loc -> qualid -> 'a +val error_global_constant_not_found_loc : Loc.t -> qualid -> 'a (** {6 Register visibility of things } *) diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 323da812d..98fd215ae 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -65,7 +65,7 @@ type grammar_constr_prod_item = concat with last parsed list if true *) let make_constr_action - (f : loc -> constr_notation_substitution -> constr_expr) pil = + (f : Loc.t -> constr_notation_substitution -> constr_expr) pil = let rec make (constrs,constrlists,binders as fullsubst) = function | [] -> Gram.action (fun loc -> f loc fullsubst) @@ -82,11 +82,11 @@ let make_constr_action Gram.action (fun (v:reference) -> make (CRef v :: constrs, constrlists, binders) tl) | ETName -> - Gram.action (fun (na:name located) -> + Gram.action (fun (na:Loc.t * name) -> make (constr_expr_of_name na :: constrs, constrlists, binders) tl) | ETBigint -> Gram.action (fun (v:Bigint.bigint) -> - make (CPrim(dummy_loc,Numeral v) :: constrs, constrlists, binders) tl) + make (CPrim(Loc.ghost,Numeral v) :: constrs, constrlists, binders) tl) | ETConstrList (_,n) -> Gram.action (fun (v:constr_expr list) -> make (constrs, v::constrlists, binders) tl) @@ -113,7 +113,7 @@ let check_cases_pattern_env loc (env,envlist,hasbinders) = else (env,envlist) let make_cases_pattern_action - (f : loc -> cases_pattern_notation_substitution -> cases_pattern_expr) pil = + (f : Loc.t -> cases_pattern_notation_substitution -> cases_pattern_expr) pil = let rec make (env,envlist,hasbinders as fullenv) = function | [] -> Gram.action (fun loc -> f loc (check_cases_pattern_env loc fullenv)) @@ -128,13 +128,13 @@ let make_cases_pattern_action make (v::env, envlist, hasbinders) tl) | ETReference -> Gram.action (fun (v:reference) -> - make (CPatAtom (dummy_loc,Some v) :: env, envlist, hasbinders) tl) + make (CPatAtom (Loc.ghost,Some v) :: env, envlist, hasbinders) tl) | ETName -> - Gram.action (fun (na:name located) -> + Gram.action (fun (na:Loc.t * name) -> make (cases_pattern_expr_of_name na :: env, envlist, hasbinders) tl) | ETBigint -> Gram.action (fun (v:Bigint.bigint) -> - make (CPatPrim (dummy_loc,Numeral v) :: env, envlist, hasbinders) tl) + make (CPatPrim (Loc.ghost,Numeral v) :: env, envlist, hasbinders) tl) | ETConstrList (_,_) -> Gram.action (fun (vl:cases_pattern_expr list) -> make (env, vl :: envlist, hasbinders) tl) diff --git a/parsing/egramml.ml b/parsing/egramml.ml index 62e7ae2bb..e86f3b385 100644 --- a/parsing/egramml.ml +++ b/parsing/egramml.ml @@ -17,7 +17,7 @@ open Vernacexpr (** Making generic actions in type generic_argument *) let make_generic_action - (f:loc -> ('b * raw_generic_argument) list -> 'a) pil = + (f:Loc.t -> ('b * raw_generic_argument) list -> 'a) pil = let rec make env = function | [] -> Gram.action (fun loc -> f loc env) @@ -37,7 +37,7 @@ let make_rule_gen mkproditem mkact pt = type grammar_prod_item = | GramTerminal of string | GramNonTerminal of - loc * argument_type * prod_entry_key * identifier option + Loc.t * argument_type * prod_entry_key * identifier option let make_prod_item = function | GramTerminal s -> (gram_token_of_string s, None) diff --git a/parsing/egramml.mli b/parsing/egramml.mli index 350e75f90..e37905271 100644 --- a/parsing/egramml.mli +++ b/parsing/egramml.mli @@ -13,7 +13,7 @@ type grammar_prod_item = | GramTerminal of string - | GramNonTerminal of Pp.loc * Genarg.argument_type * + | GramNonTerminal of Loc.t * Genarg.argument_type * Pcoq.prod_entry_key * Names.identifier option val extend_tactic_grammar : @@ -29,5 +29,5 @@ val get_extend_vernac_grammars : (** Utility function reused in Egramcoq : *) val make_rule : - (Pp.loc -> (Names.identifier * Tacexpr.raw_generic_argument) list -> 'b) -> + (Loc.t -> (Names.identifier * Tacexpr.raw_generic_argument) list -> 'b) -> grammar_prod_item list -> Pcoq.Gram.symbol list * Pcoq.Gram.action diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index f53cab6c6..f92ee4350 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -36,7 +36,7 @@ let _ = List.iter Lexer.add_keyword constr_kw let mk_cast = function (c,(_,None)) -> c | (c,(_,Some ty)) -> - let loc = join_loc (constr_loc c) (constr_loc ty) + let loc = Loc.merge (constr_loc c) (constr_loc ty) in CCast(loc, c, CastConv ty) let binders_of_names l = @@ -235,7 +235,7 @@ GEXTEND Gram | "let"; id=name; bl = binders; ty = type_cstr; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> let loc1 = - join_loc (local_binders_loc bl) (constr_loc c1) + Loc.merge (local_binders_loc bl) (constr_loc c1) in CLetIn(loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2) | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" -> @@ -422,7 +422,7 @@ GEXTEND Gram | "("; id=name; ":="; c=lconstr; ")" -> [LocalRawDef (id,c)] | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> - [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv t))] + [LocalRawDef (id,CCast (Loc.merge (constr_loc t) loc,c, CastConv t))] | "{"; id=name; "}" -> [LocalRawAssum ([id],Default Implicit,CHole (loc, None))] | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 437f0e78e..5da6ddf3d 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -180,7 +180,7 @@ GEXTEND Gram | CCast (loc, t, (CastConv ty | CastVM ty)) -> Term t, Some (Term ty) | _ -> mpv, None) | _ -> mpv, None - in Def (na, t, Option.default (Term (CHole (dummy_loc, None))) ty) + in Def (na, t, Option.default (Term (CHole (Loc.ghost, None))) ty) ] ] ; match_context_rule: diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4 index 7d7f2b10d..3bc26aa6a 100644 --- a/parsing/g_obligations.ml4 +++ b/parsing/g_obligations.ml4 @@ -46,7 +46,7 @@ open Pcoq open Prim open Constr -let sigref = mkRefC (Qualid (Pp.dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig")) +let sigref = mkRefC (Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Init.Specif.sig")) GEXTEND Gram GLOBAL: withtac; diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 927776b4e..462aa2b46 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -139,7 +139,7 @@ let mkTacCase with_evar = function (* Reinterpret numbers as a notation for terms *) | [([(ElimOnAnonHyp n)],None,(None,None))],None -> TacCase (with_evar, - (CPrim (dummy_loc, Numeral (Bigint.of_string (string_of_int n))), + (CPrim (Loc.ghost, Numeral (Bigint.of_string (string_of_int n))), NoBindings)) (* Reinterpret ident as notations for variables in the context *) (* because we don't know if they are quantified or not *) @@ -156,17 +156,17 @@ let mkTacCase with_evar = function let rec mkCLambdaN_simple_loc loc bll c = match bll with | ((loc1,_)::_ as idl,bk,t) :: bll -> - CLambdaN (loc,[idl,bk,t],mkCLambdaN_simple_loc (join_loc loc1 loc) bll c) + CLambdaN (loc,[idl,bk,t],mkCLambdaN_simple_loc (Loc.merge loc1 loc) bll c) | ([],_,_) :: bll -> mkCLambdaN_simple_loc loc bll c | [] -> c let mkCLambdaN_simple bl c = if bl=[] then c else - let loc = join_loc (fst (List.hd (pi1 (List.hd bl)))) (Constrexpr_ops.constr_loc c) in + let loc = Loc.merge (fst (List.hd (pi1 (List.hd bl)))) (Constrexpr_ops.constr_loc c) in mkCLambdaN_simple_loc loc bl c -let loc_of_ne_list l = join_loc (fst (List.hd l)) (fst (list_last l)) +let loc_of_ne_list l = Loc.merge (fst (List.hd l)) (fst (list_last l)) let map_int_or_var f = function | ArgArg x -> ArgArg (f x) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 445908fba..fbf1c64f2 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -536,16 +536,16 @@ GEXTEND Gram d = def_body -> let s = coerce_reference_to_id qid in VernacDefinition - ((Global,CanonicalStructure),(dummy_loc,s),d, + ((Global,CanonicalStructure),(Loc.ghost,s),d, (fun _ -> Recordops.declare_canonical_structure)) (* Coercions *) | IDENT "Coercion"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in - VernacDefinition ((use_locality_exp (),Coercion),(dummy_loc,s),d,Class.add_coercion_hook) + VernacDefinition ((use_locality_exp (),Coercion),(Loc.ghost,s),d,Class.add_coercion_hook) | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in - VernacDefinition ((enforce_locality_exp true,Coercion),(dummy_loc,s),d,Class.add_coercion_hook) + VernacDefinition ((enforce_locality_exp true,Coercion),(Loc.ghost,s),d,Class.add_coercion_hook) | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> VernacIdentityCoercion (enforce_locality_exp true, f, s, t) diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 7387f6933..f3b824e6d 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -27,8 +27,8 @@ open Genredexpr (* Generic xml parser without raw data *) -type attribute = string * (loc * string) -type xml = XmlTag of loc * string * attribute list * xml list +type attribute = string * (Loc.t * string) +type xml = XmlTag of Loc.t * string * attribute list * xml list let check_tags loc otag ctag = if otag <> ctag then diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index dba552e77..fcdaa6eba 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -538,7 +538,7 @@ let loct_add loct i loc = Hashtbl.add loct i loc let current_location_table = ref (loct_create ()) -type location_table = (int, loc) Hashtbl.t +type location_table = (int, Loc.t) Hashtbl.t let location_table () = !current_location_table let restore_location_table t = current_location_table := t let location_function n = loct_func !current_location_table n diff --git a/parsing/lexer.mli b/parsing/lexer.mli index 95eadfcb6..66a04a194 100644 --- a/parsing/lexer.mli +++ b/parsing/lexer.mli @@ -12,7 +12,7 @@ val add_keyword : string -> unit val remove_keyword : string -> unit val is_keyword : string -> bool -val location_function : int -> loc +val location_function : int -> Loc.t (** for coqdoc *) type location_table diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 147c5261d..2e11c1c47 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Loc open Pp open Names open Glob_term @@ -171,7 +172,7 @@ module Prim : val qualid : qualid located Gram.entry val fullyqualid : identifier list located Gram.entry val reference : reference Gram.entry - val by_notation : (loc * string * string option) Gram.entry + val by_notation : (Loc.t * string * string option) Gram.entry val smart_global : reference or_by_notation Gram.entry val dirpath : dir_path Gram.entry val ne_string : string Gram.entry @@ -242,7 +243,7 @@ module Vernac_ : end (** The main entry: reads an optional vernac command *) -val main_entry : (loc * vernac_expr) option Gram.entry +val main_entry : (Loc.t * vernac_expr) option Gram.entry (** Mapping formal entries into concrete ones *) 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<let cont := $k in cont $x>> 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) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 4b7f9187f..eca91138e 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Compat open Pp open Errors open Util @@ -68,7 +67,7 @@ let error_needs_inversion env x t = module type S = sig val compile_cases : - loc -> case_style -> + Loc.t -> case_style -> (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref -> type_constraint -> env -> glob_constr option * tomatch_tuples * cases_clauses -> @@ -102,7 +101,7 @@ let msg_may_need_inversion () = (* Utils *) let make_anonymous_patvars n = - list_make n (PatVar (dummy_loc,Anonymous)) + list_make n (PatVar (Loc.ghost,Anonymous)) (* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *) @@ -128,7 +127,7 @@ type 'a equation = { patterns : cases_pattern list; rhs : 'a rhs; alias_stack : name list; - eqn_loc : loc; + eqn_loc : Loc.t; used : bool ref } type 'a matrix = 'a equation list @@ -178,7 +177,7 @@ and build_glob_pattern args = function | Top -> args | MakeConstructor (pci, rh) -> glob_pattern_of_partial_history - [PatCstr (dummy_loc, pci, args, Anonymous)] rh + [PatCstr (Loc.ghost, pci, args, Anonymous)] rh let complete_history = glob_pattern_of_partial_history [] @@ -188,12 +187,12 @@ let rec pop_history_pattern = function | Continuation (0, l, Top) -> Result (List.rev l) | Continuation (0, l, MakeConstructor (pci, rh)) -> - feed_history (PatCstr (dummy_loc,pci,List.rev l,Anonymous)) rh + feed_history (PatCstr (Loc.ghost,pci,List.rev l,Anonymous)) rh | _ -> anomaly "Constructor not yet filled with its arguments" let pop_history h = - feed_history (PatVar (dummy_loc, Anonymous)) h + feed_history (PatVar (Loc.ghost, Anonymous)) h (* Builds a continuation expecting [n] arguments and building [ci] applied to this [n] arguments *) @@ -251,7 +250,7 @@ type 'a pattern_matching_problem = tomatch : tomatch_stack; history : pattern_continuation; mat : 'a matrix; - caseloc : loc; + caseloc : Loc.t; casestyle : case_style; typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment } @@ -280,7 +279,7 @@ let inductive_template evdref env tmloc ind = let arsign = get_full_arity_sign env ind in let hole_source = match tmloc with | Some loc -> fun i -> (loc, Evar_kinds.TomatchTypeParameter (ind,i)) - | None -> fun _ -> (dummy_loc, Evar_kinds.InternalHole) in + | None -> fun _ -> (Loc.ghost, Evar_kinds.InternalHole) in let (_,evarl,_) = List.fold_right (fun (na,b,ty) (subst,evarl,n) -> @@ -358,7 +357,7 @@ let coerce_to_indtype typing_fun evdref env matx tomatchl = (************************************************************************) (* Utils *) -let mkExistential env ?(src=(dummy_loc,Evar_kinds.InternalHole)) evdref = +let mkExistential env ?(src=(Loc.ghost,Evar_kinds.InternalHole)) evdref = e_new_evar evdref env ~src:src (new_Type ()) let evd_comb2 f evdref x y = @@ -390,7 +389,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) = let _ = e_cumul pb.env pb.evdref indt typ in current else - (evd_comb2 (Coercion.inh_conv_coerce_to dummy_loc pb.env) + (evd_comb2 (Coercion.inh_conv_coerce_to Loc.ghost pb.env) pb.evdref (make_judge current typ) indt).uj_val in let sigma = !(pb.evdref) in (current,try_find_ind pb.env sigma indt names)) @@ -914,7 +913,7 @@ let adjust_impossible_cases pb pred tomatch submat = let default = (coq_unit_judge ()).uj_type in pb.evdref := Evd.define evk default !(pb.evdref); (* we add an "assert false" case *) - let pats = List.map (fun _ -> PatVar (dummy_loc,Anonymous)) tomatch in + let pats = List.map (fun _ -> PatVar (Loc.ghost,Anonymous)) tomatch in let aliasnames = map_succeed (function Alias _ | NonDepAlias -> Anonymous | _ -> failwith"") tomatch in @@ -924,7 +923,7 @@ let adjust_impossible_cases pb pred tomatch submat = avoid_ids = []; it = None }; alias_stack = Anonymous::aliasnames; - eqn_loc = dummy_loc; + eqn_loc = Loc.ghost; used = ref false } ] | _ -> submat @@ -1207,7 +1206,7 @@ let build_branch current realargs deps (realnames,curname) pb arsign eqns const_ let submat = adjust_impossible_cases pb pred tomatch submat in if submat = [] then raise_pattern_matching_error - (dummy_loc, pb.env, NonExhaustive (complete_history history)); + (Loc.ghost, pb.env, NonExhaustive (complete_history history)); typs, { pb with @@ -1531,16 +1530,16 @@ let build_tycon loc env tycon_env subst tycon extenv evdref t = let build_inversion_problem loc env sigma tms t = let make_patvar t (subst,avoid) = let id = next_name_away (named_hd env t Anonymous) avoid in - PatVar (dummy_loc,Name id), ((id,t)::subst, id::avoid) in + PatVar (Loc.ghost,Name id), ((id,t)::subst, id::avoid) in let rec reveal_pattern t (subst,avoid as acc) = match kind_of_term (whd_betadeltaiota env sigma t) with - | Construct cstr -> PatCstr (dummy_loc,cstr,[],Anonymous), acc + | Construct cstr -> PatCstr (Loc.ghost,cstr,[],Anonymous), acc | App (f,v) when isConstruct f -> let cstr = destConstruct f in let n = constructor_nrealargs env cstr in let l = list_lastn n (Array.to_list v) in let l,acc = list_fold_map' reveal_pattern l acc in - PatCstr (dummy_loc,cstr,l,Anonymous), acc + PatCstr (Loc.ghost,cstr,l,Anonymous), acc | _ -> make_patvar t acc in let rec aux n env acc_sign tms acc = match tms with @@ -1597,7 +1596,7 @@ let build_inversion_problem loc env sigma tms t = let eqn1 = { patterns = patl; alias_stack = []; - eqn_loc = dummy_loc; + eqn_loc = Loc.ghost; used = ref false; rhs = { rhs_env = pb_env; (* we assume all vars are used; in practice we discard dependent @@ -1610,9 +1609,9 @@ let build_inversion_problem loc env sigma tms t = type constraints are incompatible with the constraints on the inductive types of the multiple terms matched in Xi *) let eqn2 = - { patterns = List.map (fun _ -> PatVar (dummy_loc,Anonymous)) patl; + { patterns = List.map (fun _ -> PatVar (Loc.ghost,Anonymous)) patl; alias_stack = []; - eqn_loc = dummy_loc; + eqn_loc = Loc.ghost; used = ref false; rhs = { rhs_env = pb_env; rhs_vars = []; @@ -1827,7 +1826,7 @@ let mk_JMeq typ x typ' y = mkApp (delayed_force coq_JMeq_ind, [| typ; x ; typ'; y |]) let mk_JMeq_refl typ x = mkApp (delayed_force coq_JMeq_refl, [| typ; x |]) -let hole = GHole (dummy_loc, Evar_kinds.QuestionMark (Evar_kinds.Define true)) +let hole = GHole (Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define true)) let constr_of_pat env isevars arsign pat avoid = let rec typ env (ty, realargs) pat avoid = @@ -1919,13 +1918,13 @@ let vars_of_ctx ctx = match b with | Some t' when kind_of_term t' = Rel 0 -> prev, - (GApp (dummy_loc, - (GRef (dummy_loc, delayed_force coq_eq_refl_ref)), - [hole; GVar (dummy_loc, prev)])) :: vars + (GApp (Loc.ghost, + (GRef (Loc.ghost, delayed_force coq_eq_refl_ref)), + [hole; GVar (Loc.ghost, prev)])) :: vars | _ -> match na with Anonymous -> raise (Invalid_argument "vars_of_ctx") - | Name n -> n, GVar (dummy_loc, n) :: vars) + | Name n -> n, GVar (Loc.ghost, n) :: vars) ctx (id_of_string "vars_of_ctx_error", []) in List.rev y @@ -2060,13 +2059,13 @@ let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity = let branch_name = id_of_string ("program_branch_" ^ (string_of_int !i)) in let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in let branch = - let bref = GVar (dummy_loc, branch_name) in + let bref = GVar (Loc.ghost, branch_name) in match vars_of_ctx rhs_rels with [] -> bref - | l -> GApp (dummy_loc, bref, l) + | l -> GApp (Loc.ghost, bref, l) in let branch = match ineqs with - Some _ -> GApp (dummy_loc, branch, [ hole ]) + Some _ -> GApp (Loc.ghost, branch, [ hole ]) | None -> branch in incr i; diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 7add91c16..6e2b823db 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -31,24 +31,24 @@ type pattern_matching_error = exception PatternMatchingError of env * pattern_matching_error -val raise_pattern_matching_error : (loc * env * pattern_matching_error) -> 'a +val raise_pattern_matching_error : (Loc.t * env * pattern_matching_error) -> 'a -val error_wrong_numarg_constructor_loc : loc -> env -> constructor -> int -> 'a +val error_wrong_numarg_constructor_loc : Loc.t -> env -> constructor -> int -> 'a -val error_wrong_numarg_inductive_loc : loc -> env -> inductive -> int -> 'a +val error_wrong_numarg_inductive_loc : Loc.t -> env -> inductive -> int -> 'a -val error_bad_constructor_loc : loc -> constructor -> inductive -> 'a +val error_bad_constructor_loc : Loc.t -> constructor -> inductive -> 'a -val error_bad_pattern_loc : loc -> constructor -> constr -> 'a +val error_bad_pattern_loc : Loc.t -> constructor -> constr -> 'a -val error_wrong_predicate_arity_loc : loc -> env -> constr -> constr -> constr -> 'a +val error_wrong_predicate_arity_loc : Loc.t -> env -> constr -> constr -> constr -> 'a val error_needs_inversion : env -> constr -> types -> 'a (** {6 Compilation primitive. } *) val compile_cases : - loc -> case_style -> + Loc.t -> case_style -> (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref -> type_constraint -> env -> glob_constr option * tomatch_tuples * cases_clauses -> @@ -75,7 +75,7 @@ type 'a equation = { patterns : cases_pattern list; rhs : 'a rhs; alias_stack : name list; - eqn_loc : loc; + eqn_loc : Loc.t; used : bool ref } type 'a matrix = 'a equation list @@ -110,7 +110,7 @@ type 'a pattern_matching_problem = tomatch : tomatch_stack; history : pattern_continuation; mat : 'a matrix; - caseloc : loc; + caseloc : Loc.t; casestyle : case_style; typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment } diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index b2e41841e..189651735 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -26,36 +26,36 @@ val inh_app_fun : (** [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it inserts a coercion into [j], if needed, in such a way it gets as type a sort; it fails if no coercion is applicable *) -val inh_coerce_to_sort : loc -> +val inh_coerce_to_sort : Loc.t -> env -> evar_map -> unsafe_judgment -> evar_map * unsafe_type_judgment (** [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it inserts a coercion into [j], if needed, in such a way it gets as type its base type (the notion depends on the coercion system) *) -val inh_coerce_to_base : loc -> +val inh_coerce_to_base : Loc.t -> env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment (** [inh_coerce_to_prod env isevars t] coerces [t] to a product type *) -val inh_coerce_to_prod : loc -> +val inh_coerce_to_prod : Loc.t -> env -> evar_map -> types -> evar_map * types -(** [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type +(** [inh_conv_coerce_to Loc.t env isevars j t] coerces [j] to an object of type [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and [j.uj_type] are convertible; it fails if no coercion is applicable *) -val inh_conv_coerce_to : loc -> +val inh_conv_coerce_to : Loc.t -> env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment -val inh_conv_coerce_rigid_to : loc -> +val inh_conv_coerce_rigid_to : Loc.t -> env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment (** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t] is coercible to an object of type [t'] adding evar constraints if needed; it fails if no coercion exists *) -val inh_conv_coerces_to : loc -> +val inh_conv_coerces_to : Loc.t -> env -> evar_map -> types -> types -> evar_map (** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases pattern [pat] typed in [ind1] into a pattern typed in [ind2]; raises [Not_found] if no coercion found *) val inh_pattern_coerce_to : - loc -> cases_pattern -> inductive -> inductive -> cases_pattern + Loc.t -> cases_pattern -> inductive -> inductive -> cases_pattern diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index b6d460a85..7ed29ba39 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -30,7 +30,7 @@ open Mod_subst open Misctypes open Decl_kinds -let dl = dummy_loc +let dl = Loc.ghost (** Should we keep details of universes during detyping ? *) let print_universes = ref false @@ -687,12 +687,12 @@ let rec subst_glob_constr subst raw = let simple_cases_matrix_of_branches ind brs = List.map (fun (i,n,b) -> let nal,c = it_destRLambda_or_LetIn_names n b in - let mkPatVar na = PatVar (dummy_loc,na) in - let p = PatCstr (dummy_loc,(ind,i+1),List.map mkPatVar nal,Anonymous) in + let mkPatVar na = PatVar (Loc.ghost,na) in + let p = PatCstr (Loc.ghost,(ind,i+1),List.map mkPatVar nal,Anonymous) in let ids = map_succeed Nameops.out_name nal in - (dummy_loc,ids,[p],c)) + (Loc.ghost,ids,[p],c)) brs let return_type_of_predicate ind nrealargs_ctxt pred = let nal,p = it_destRLambda_or_LetIn_names (nrealargs_ctxt+1) pred in - (List.hd nal, Some (dummy_loc, ind, List.tl nal)), Some p + (List.hd nal, Some (Loc.ghost, ind, List.tl nal)), Some p diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 10f23b1b2..1c6127361 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -34,7 +34,7 @@ val detype : bool -> identifier list -> names_context -> constr -> glob_constr val detype_case : bool -> ('a -> glob_constr) -> (constructor array -> int array -> 'a array -> - (loc * identifier list * cases_pattern list * glob_constr) list) -> + (Loc.t * identifier list * cases_pattern list * glob_constr) list) -> ('a -> int -> bool) -> identifier list -> inductive * case_style * int array * int -> 'a option -> 'a -> 'a array -> glob_constr @@ -48,7 +48,7 @@ val detype_rel_context : constr option -> identifier list -> names_context -> val lookup_name_as_displayed : env -> constr -> identifier -> int option val lookup_index_as_renamed : env -> constr -> int -> int option -val set_detype_anonymous : (loc -> int -> glob_constr) -> unit +val set_detype_anonymous : (Loc.t -> int -> glob_constr) -> unit val force_wildcard : unit -> bool val synthetize_type : unit -> bool diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 127e52e9a..a01140795 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -540,7 +540,7 @@ and conv_record trs env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) List.fold_left (fun (i,ks,m) b -> if m=n then (i,t2::ks, m-1) else - let dloc = (dummy_loc,Evar_kinds.InternalHole) in + let dloc = (Loc.ghost,Evar_kinds.InternalHole) in let (i',ev) = new_evar i env ~src:dloc (substl ks b) in (i', ev :: ks, m - 1)) (evd,[],List.length bs - 1) bs diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index bd47badfe..b8f216ad4 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -308,7 +308,7 @@ let push_rel_context_to_named_context env typ = * Entry points to define new evars * *------------------------------------*) -let default_source = (dummy_loc,Evar_kinds.InternalHole) +let default_source = (Loc.ghost,Evar_kinds.InternalHole) let new_pure_evar evd sign ?(src=default_source) ?filter ?candidates typ = let newevk = new_untyped_evar() in @@ -338,7 +338,7 @@ let new_type_evar ?src ?filter evd env = new_evar evd' env ?src ?filter (mkSort s) (* The same using side-effect *) -let e_new_evar evdref env ?(src=(dummy_loc,Evar_kinds.InternalHole)) ?filter ?candidates ty = +let e_new_evar evdref env ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?filter ?candidates ty = let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates ty in evdref := evd'; ev @@ -1962,7 +1962,7 @@ let define_pure_evar_as_lambda env evd evk = let evd1,(na,dom,rng) = match kind_of_term typ with | Prod (na,dom,rng) -> (evd,(na,dom,rng)) | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ - | _ -> error_not_product_loc dummy_loc env evd typ in + | _ -> error_not_product_loc Loc.ghost env evd typ in let avoid = ids_of_named_context (evar_context evi) in let id = next_name_away_with_default_using_types "x" na avoid (whd_evar evd dom) in diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index ea0f063fe..77985c8d7 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -29,18 +29,18 @@ val new_untyped_evar : unit -> existential_key (** {6 Creating a fresh evar given their type and context} *) val new_evar : - evar_map -> env -> ?src:loc * Evar_kinds.t -> ?filter:bool list -> + evar_map -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list -> ?candidates:constr list -> types -> evar_map * constr (** the same with side-effects *) val e_new_evar : - evar_map ref -> env -> ?src:loc * Evar_kinds.t -> ?filter:bool list -> + evar_map ref -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list -> ?candidates:constr list -> types -> constr (** Create a new Type existential variable, as we keep track of them during type-checking and unification. *) val new_type_evar : - ?src:loc * Evar_kinds.t -> ?filter:bool list -> evar_map -> env -> evar_map * constr + ?src:Loc.t * Evar_kinds.t -> ?filter:bool list -> evar_map -> env -> evar_map * constr (** Create a fresh evar in a context different from its definition context: [new_evar_instance sign evd ty inst] creates a new evar of context @@ -49,7 +49,7 @@ val new_type_evar : of [inst] are typed in the occurrence context and their type (seen as a telescope) is [sign] *) val new_evar_instance : - named_context_val -> evar_map -> types -> ?src:loc * Evar_kinds.t -> ?filter:bool list -> ?candidates:constr list -> constr list -> evar_map * constr + named_context_val -> evar_map -> types -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list -> ?candidates:constr list -> constr list -> evar_map * constr val make_pure_subst : evar_info -> constr array -> (identifier * constr) list @@ -158,7 +158,7 @@ val empty_valcon : val_constraint val mk_valcon : constr -> val_constraint val split_tycon : - loc -> env -> evar_map -> type_constraint -> + Loc.t -> env -> evar_map -> type_constraint -> evar_map * (name * type_constraint * type_constraint) val valcon_of_tycon : type_constraint -> val_constraint diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 0197af56c..9f47987f4 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -37,7 +37,7 @@ type evar_info = { evar_hyps : named_context_val; evar_body : evar_body; evar_filter : bool list; - evar_source : Evar_kinds.t located; + evar_source : Evar_kinds.t Loc.located; evar_candidates : constr list option; (* if not None, list of allowed instances *) evar_extra : Store.t } @@ -46,7 +46,7 @@ let make_evar hyps ccl = { evar_hyps = hyps; evar_body = Evar_empty; evar_filter = List.map (fun _ -> true) (named_context_of_val hyps); - evar_source = (dummy_loc,Evar_kinds.InternalHole); + evar_source = (Loc.ghost,Evar_kinds.InternalHole); evar_candidates = None; evar_extra = Store.empty } @@ -420,7 +420,7 @@ let define evk body evd = | [] -> evd.last_mods | _ -> ExistentialSet.add evk evd.last_mods } -let evar_declare hyps evk ty ?(src=(dummy_loc,Evar_kinds.InternalHole)) ?filter ?candidates evd = +let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?filter ?candidates evd = let filter = if filter = None then List.map (fun _ -> true) (named_context_of_val hyps) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 70a18b54a..f17788871 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Loc open Pp open Names open Term @@ -177,7 +178,7 @@ val defined_evars : evar_map -> evar_map It optimizes the call of {!Evd.fold} to [f] and [undefined_evars m] *) val fold_undefined : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a val evar_declare : - named_context_val -> evar -> types -> ?src:loc * Evar_kinds.t -> + named_context_val -> evar -> types -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list -> ?candidates:constr list -> evar_map -> evar_map val evar_source : existential_key -> evar_map -> Evar_kinds.t located diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 6a26fe1d4..4caf4d531 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -19,12 +19,12 @@ open Glob_term (** Operations on [glob_constr] *) -val cases_pattern_loc : cases_pattern -> loc +val cases_pattern_loc : cases_pattern -> Loc.t val cases_predicate_names : tomatch_tuples -> name list (** Apply one argument to a glob_constr *) -val mkGApp : loc -> glob_constr -> glob_constr -> glob_constr +val mkGApp : Loc.t -> glob_constr -> glob_constr -> glob_constr val map_glob_constr : (glob_constr -> glob_constr) -> glob_constr -> glob_constr @@ -37,7 +37,7 @@ val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit val occur_glob_constr : identifier -> glob_constr -> bool val free_glob_vars : glob_constr -> identifier list -val loc_of_glob_constr : glob_constr -> loc +val loc_of_glob_constr : glob_constr -> Loc.t (** Conversion from glob_constr to cases pattern, if possible diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli index 123d307de..45a14a3d4 100644 --- a/pretyping/miscops.mli +++ b/pretyping/miscops.mli @@ -15,7 +15,7 @@ val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type (** Printing of [intro_pattern] *) -val pr_intro_pattern : intro_pattern_expr Pp.located -> Pp.std_ppcmds +val pr_intro_pattern : intro_pattern_expr Loc.located -> Pp.std_ppcmds val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds (** Printing of [move_location] *) diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index e0cc2dec3..f34b8af3d 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Compat open Errors open Util open Names diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 2410fb7ca..23b9c4d10 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -58,33 +58,33 @@ val jv_nf_betaiotaevar : (** Raising errors *) val error_actual_type_loc : - loc -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b + Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b val error_cant_apply_not_functional_loc : - loc -> env -> Evd.evar_map -> + Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> unsafe_judgment list -> 'b val error_cant_apply_bad_type_loc : - loc -> env -> Evd.evar_map -> int * constr * constr -> + Loc.t -> env -> Evd.evar_map -> int * constr * constr -> unsafe_judgment -> unsafe_judgment list -> 'b val error_case_not_inductive_loc : - loc -> env -> Evd.evar_map -> unsafe_judgment -> 'b + Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b val error_ill_formed_branch_loc : - loc -> env -> Evd.evar_map -> + Loc.t -> env -> Evd.evar_map -> constr -> constructor -> constr -> constr -> 'b val error_number_branches_loc : - loc -> env -> Evd.evar_map -> + Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> int -> 'b val error_ill_typed_rec_body_loc : - loc -> env -> Evd.evar_map -> + Loc.t -> env -> Evd.evar_map -> int -> name array -> unsafe_judgment array -> types array -> 'b val error_not_a_type_loc : - loc -> env -> Evd.evar_map -> unsafe_judgment -> 'b + Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b @@ -93,10 +93,10 @@ val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b val error_not_clean : - env -> Evd.evar_map -> existential_key -> constr -> loc * Evar_kinds.t -> 'b + env -> Evd.evar_map -> existential_key -> constr -> Loc.t * Evar_kinds.t -> 'b val error_unsolvable_implicit : - loc -> env -> Evd.evar_map -> Evd.evar_info -> Evar_kinds.t -> + Loc.t -> env -> Evd.evar_map -> Evd.evar_info -> Evar_kinds.t -> Evd.unsolvability_explanation option -> 'b val error_cannot_unify : env -> Evd.evar_map -> constr * constr -> 'b @@ -115,16 +115,16 @@ val error_non_linear_unification : env -> Evd.evar_map -> (** {6 Ml Case errors } *) val error_cant_find_case_type_loc : - loc -> env -> Evd.evar_map -> constr -> 'b + Loc.t -> env -> Evd.evar_map -> constr -> 'b (** {6 Pretyping errors } *) val error_unexpected_type_loc : - loc -> env -> Evd.evar_map -> constr -> constr -> 'b + Loc.t -> env -> Evd.evar_map -> constr -> constr -> 'b val error_not_product_loc : - loc -> env -> Evd.evar_map -> constr -> 'b + Loc.t -> env -> Evd.evar_map -> constr -> 'b (** {6 Error in conversion from AST to glob_constr } *) -val error_var_not_found_loc : loc -> identifier -> 'b +val error_var_not_found_loc : Loc.t -> identifier -> 'b diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index bcd2a1ad1..a494e2f93 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -21,7 +21,6 @@ (* Secondary maintenance: collective *) -open Compat open Pp open Errors open Util @@ -74,7 +73,7 @@ let search_guard loc env possible_indexes fixdefs = let indexes = Array.of_list (List.map List.hd possible_indexes) in let fix = ((indexes, 0),fixdefs) in (try check_fix env fix with - | e -> if loc = dummy_loc then raise e else Loc.raise loc e); + | e -> if loc = Loc.ghost then raise e else Loc.raise loc e); indexes else (* we now search recursively amoungst all combinations *) @@ -87,7 +86,7 @@ let search_guard loc env possible_indexes fixdefs = with TypeError _ -> ()) (list_combinations possible_indexes); let errmsg = "Cannot guess decreasing argument of fix." in - if loc = dummy_loc then error errmsg else + if loc = Loc.ghost then error errmsg else user_err_loc (loc,"search_guard", Pp.str errmsg) with Found indexes -> indexes) @@ -428,7 +427,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function | _ -> let hj = pretype empty_tycon env evdref lvar c in error_cant_apply_not_functional_loc - (join_loc floc argloc) env !evdref + (Loc.merge floc argloc) env !evdref resj [hj] in let resj = apply_rec env 1 fj candargs args in diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 9401edc2d..776e6e94e 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -24,7 +24,7 @@ open Misctypes (** An auxiliary function for searching for fixpoint guard indexes *) val search_guard : - Pp.loc -> env -> int list list -> rec_declaration -> int array + Loc.t -> env -> int list list -> rec_declaration -> int array type typing_constraint = OfType of types option | IsType diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index fee55e72a..5d1e4264a 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -16,7 +16,6 @@ open Environ open Nametab open Mod_subst open Constrexpr -open Compat open Pp open Util open Globnames @@ -26,8 +25,8 @@ type contexts = Parameters | Properties type typeclass_error = | NotAClass of constr - | UnboundMethod of global_reference * identifier located (* Class name, method *) - | NoInstance of identifier located * constr list + | UnboundMethod of global_reference * identifier Loc.located (* Class name, method *) + | NoInstance of identifier Loc.located * constr list | UnsatisfiableConstraints of evar_map * (existential_key * Evar_kinds.t) option | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *) diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index a05258de7..f14bfef22 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Loc open Names open Decl_kinds open Term diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 4bf0928dc..27e5864b3 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -123,7 +123,7 @@ let pose_all_metas_as_evars env evd t = | None -> let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in let ty = if mvs = Evd.Metaset.empty then ty else aux ty in - let ev = Evarutil.e_new_evar evdref env ~src:(dummy_loc,Evar_kinds.GoalEvar) ty in + let ev = Evarutil.e_new_evar evdref env ~src:(Loc.ghost,Evar_kinds.GoalEvar) ty in evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref; ev) | _ -> @@ -782,7 +782,7 @@ let applyHead env evd n c = match kind_of_term (whd_betadeltaiota env evd cty) with | Prod (_,c1,c2) -> let (evd',evar) = - Evarutil.new_evar evd env ~src:(dummy_loc,Evar_kinds.GoalEvar) c1 in + Evarutil.new_evar evd env ~src:(Loc.ghost,Evar_kinds.GoalEvar) c1 in apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd' | _ -> error "Apply_Head_Then" in @@ -797,7 +797,7 @@ let is_mimick_head ts f = let try_to_coerce env evd c cty tycon = let j = make_judge c cty in - let (evd',j') = inh_conv_coerce_rigid_to dummy_loc env evd j tycon in + let (evd',j') = inh_conv_coerce_rigid_to Loc.ghost env evd j tycon in let evd' = Evarconv.consider_remaining_unif_problems env evd' in let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in (evd',j'.uj_val) diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 87815dc0b..bdf69c9cf 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -104,7 +104,7 @@ let pr_com_at n = if Flags.do_beautify() && n <> 0 then comment n else mt() -let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp) +let pr_with_comments loc pp = Loc.pr_located (fun x -> x) (loc,pp) let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c) @@ -137,14 +137,14 @@ let pr_opt_type_spc pr = function | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t let pr_lident (loc,id) = - if loc <> dummy_loc then - let (b,_) = unloc loc in - pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id) + if loc <> Loc.ghost then + let (b,_) = Loc.unloc loc in + Loc.pr_located pr_id (Loc.make_loc (b,b+String.length(string_of_id id)),id) else pr_id id let pr_lname = function (loc,Name id) -> pr_lident (loc,id) - | lna -> pr_located pr_name lna + | lna -> Loc.pr_located pr_name lna let pr_or_var pr = function | ArgArg x -> pr x @@ -213,8 +213,8 @@ let pr_eqn pr (loc,pl,rhs) = pr_sep_com spc (pr ltop) rhs)) let begin_of_binder = function - LocalRawDef((loc,_),_) -> fst (unloc loc) - | LocalRawAssum((loc,_)::_,_,_) -> fst (unloc loc) + LocalRawDef((loc,_),_) -> fst (Loc.unloc loc) + | LocalRawAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc) | _ -> assert false let begin_of_binders = function @@ -260,7 +260,7 @@ let pr_binder_among_many pr_c = function | LocalRawDef (na,c) -> let c,topt = match c with | CCast(_,c, (CastConv t|CastVM t)) -> c, t - | _ -> c, CHole (dummy_loc, None) in + | _ -> c, CHole (Loc.ghost, None) in surround (pr_lname na ++ pr_opt_type pr_c topt ++ str":=" ++ cut() ++ pr_c c) diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 304e5958e..598bb3ed3 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Loc open Pp open Environ open Term @@ -34,7 +35,7 @@ val pr_metaid : identifier -> std_ppcmds val pr_lident : identifier located -> std_ppcmds val pr_lname : name located -> std_ppcmds -val pr_with_comments : loc -> std_ppcmds -> std_ppcmds +val pr_with_comments : Loc.t -> std_ppcmds -> std_ppcmds val pr_com_at : int -> std_ppcmds val pr_sep_com : (unit -> std_ppcmds) -> diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 14cfe2ffc..815ee6e5c 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -357,7 +357,7 @@ let pr_as_ipat = function let pr_as_name = function | Anonymous -> mt () - | Name id -> str " as " ++ pr_lident (dummy_loc,id) + | Name id -> str " as " ++ pr_lident (Loc.ghost,id) let pr_pose_as_style prc na c = spc() ++ prc c ++ pr_as_name na @@ -479,7 +479,7 @@ let pr_funvar = function let pr_let_clause k pr (id,(bl,t)) = hov 0 (str k ++ pr_lident id ++ prlist pr_funvar bl ++ - str " :=" ++ brk (1,1) ++ pr (TacArg (dummy_loc,t))) + str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.ghost,t))) let pr_let_clauses recflag pr = function | hd::tl -> @@ -952,7 +952,7 @@ and pr_tacarg = function str "external" ++ spc() ++ qs com ++ spc() ++ qs req ++ spc() ++ prlist_with_sep spc pr_tacarg la | (TacCall _|Tacexp _|Integer _) as a -> - str "ltac:" ++ pr_tac (latom,E) (TacArg (dummy_loc,a)) + str "ltac:" ++ pr_tac (latom,E) (TacArg (Loc.ghost,a)) in (pr_tac, pr_match_rule) @@ -961,7 +961,7 @@ let strip_prod_binders_glob_constr n (ty,_) = if n=0 then (List.rev acc, (ty,None)) else match ty with Glob_term.GProd(loc,na,Explicit,a,b) -> - strip_ty (([dummy_loc,na],(a,None))::acc) (n-1) b + strip_ty (([Loc.ghost,na],(a,None))::acc) (n-1) b | _ -> error "Cannot translate fix tactic: not enough products" in strip_ty [] n ty @@ -970,7 +970,7 @@ let strip_prod_binders_constr n ty = if n=0 then (List.rev acc, ty) else match Term.kind_of_term ty with Term.Prod(na,a,b) -> - strip_ty (([dummy_loc,na],a)::acc) (n-1) b + strip_ty (([Loc.ghost,na],a)::acc) (n-1) b | _ -> error "Cannot translate fix tactic: not enough products" in strip_ty [] n ty diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 07838edcd..efca60f00 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -10,6 +10,9 @@ open Pp open Names open Nameops open Nametab + +let pr_located = Loc.pr_located + open Compat open Errors open Util @@ -30,7 +33,7 @@ open Declaremods let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr let pr_lident (loc,id) = - if loc <> dummy_loc then + if loc <> Loc.ghost then let (b,_) = unloc loc in pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id) else pr_id id @@ -41,7 +44,7 @@ let string_of_fqid fqid = let pr_fqid fqid = str (string_of_fqid fqid) let pr_lfqid (loc,fqid) = - if loc <> dummy_loc then + if loc <> Loc.ghost then let (b,_) = unloc loc in pr_located pr_fqid (make_loc (b,b+String.length(string_of_fqid fqid)),fqid) else diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 2e8cc4023..5e65bde25 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -435,7 +435,7 @@ let gallina_print_constant_with_infos sp = let gallina_print_syntactic_def kn = let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn and (vars,a) = Syntax_def.search_syntactic_definition kn in - let c = Notation_ops.glob_constr_of_notation_constr dummy_loc a in + let c = Notation_ops.glob_constr_of_notation_constr Loc.ghost a in hov 2 (hov 4 (str "Notation " ++ pr_qualid qid ++ diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 23a21414d..fb1900f2f 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -320,7 +320,7 @@ let clenv_pose_metas_as_evars clenv dep_mvs = if occur_meta ty then fold clenv (mvs@[mv]) else let (evd,evar) = - new_evar clenv.evd (cl_env clenv) ~src:(dummy_loc,Evar_kinds.GoalEvar) ty in + new_evar clenv.evd (cl_env clenv) ~src:(Loc.ghost,Evar_kinds.GoalEvar) ty in let clenv = clenv_assign mv evar {clenv with evd=evd} in fold clenv mvs in fold clenv dep_mvs diff --git a/proofs/goal.ml b/proofs/goal.ml index 9b3e90198..e7a6bce6c 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -154,7 +154,7 @@ module Refinable = struct let my_type = Retyping.get_type_of env !rdefs t in let j = Environ.make_judge t my_type in let (new_defs,j') = - Coercion.inh_conv_coerce_to (Pp.dummy_loc) env !rdefs j typ + Coercion.inh_conv_coerce_to (Loc.ghost) env !rdefs j typ in rdefs := new_defs; j'.Environ.uj_val @@ -498,7 +498,7 @@ module V82 = struct Evd.evar_filter = List.map (fun _ -> true) (Environ.named_context_of_val hyps); Evd.evar_body = Evd.Evar_empty; - Evd.evar_source = (Pp.dummy_loc,Evar_kinds.GoalEvar); + Evd.evar_source = (Loc.ghost,Evar_kinds.GoalEvar); Evd.evar_candidates = None; Evd.evar_extra = extra } in diff --git a/proofs/logic.ml b/proofs/logic.ml index 3a5d2139b..8247481e0 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Compat open Pp open Errors open Util diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 583e40c00..60d24a50c 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Loc open Pp open Names open Term diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 8dbb63739..c394ab35b 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -35,7 +35,7 @@ val check_no_pending_proof : unit -> unit val get_current_proof_name : unit -> Names.identifier val get_all_proof_names : unit -> Names.identifier list -val discard : Names.identifier Pp.located -> unit +val discard : Names.identifier Loc.located -> unit val discard_current : unit -> unit val discard_all : unit -> unit diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 61e89ac1d..c4325fa54 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -98,8 +98,8 @@ type ltac_call_kind = | LtacConstrInterp of glob_constr * (extended_patvar_map * (identifier * identifier option) list) -type ltac_trace = (int * loc * ltac_call_kind) list +type ltac_trace = (int * Loc.t * ltac_call_kind) list -exception LtacLocated of (int * ltac_call_kind * ltac_trace * loc) * exn +exception LtacLocated of (int * ltac_call_kind * ltac_trace * Loc.t) * exn let abstract_tactic_box = ref (ref None) diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 3476eaaab..ac29fa877 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -128,8 +128,8 @@ type ltac_call_kind = | LtacConstrInterp of glob_constr * (extended_patvar_map * (identifier * identifier option) list) -type ltac_trace = (int * loc * ltac_call_kind) list +type ltac_trace = (int * Loc.t * ltac_call_kind) list -exception LtacLocated of (int * ltac_call_kind * ltac_trace * loc) * exn +exception LtacLocated of (int * ltac_call_kind * ltac_trace * Loc.t) * exn val abstract_tactic_box : atomic_tactic_expr option ref ref diff --git a/proofs/proofview.ml b/proofs/proofview.ml index ff0e8de41..fc752cd33 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Compat - (* The proofview datastructure is a pure datastructure underlying the notion of proof (namely, a proof is a proofview which can evolve and has safety mechanisms attached). diff --git a/proofs/refiner.ml b/proofs/refiner.ml index cb588af2d..dc58abbb2 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Compat open Pp open Errors open Util @@ -38,10 +37,10 @@ let abstract_tactic_expr ?(dflt=false) te tacfun gls = let abstract_tactic ?(dflt=false) te = !abstract_tactic_box := Some te; - abstract_tactic_expr ~dflt (Tacexpr.TacAtom (dummy_loc,te)) + abstract_tactic_expr ~dflt (Tacexpr.TacAtom (Loc.ghost,te)) let abstract_extended_tactic ?(dflt=false) s args = - abstract_tactic ~dflt (Tacexpr.TacExtend (dummy_loc, s, args)) + abstract_tactic ~dflt (Tacexpr.TacExtend (Loc.ghost, s, args)) let refiner = function | Prim pr -> diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli index 74c831487..eca9ef807 100644 --- a/proofs/tactic_debug.mli +++ b/proofs/tactic_debug.mli @@ -18,7 +18,7 @@ open Term Currently, it is quite simple and we can hope to have, in the future, a more complete panel of commands dedicated to a proof assistant framework *) -val set_tactic_printer : (glob_tactic_expr ->Pp.std_ppcmds) -> unit +val set_tactic_printer : (glob_tactic_expr -> Pp.std_ppcmds) -> unit val set_match_pattern_printer : (env -> constr_pattern match_pattern -> Pp.std_ppcmds) -> unit val set_match_rule_printer : @@ -78,4 +78,4 @@ val db_logic_failure : debug_info -> exn -> unit (** Prints a logic failure message for a rule *) val db_breakpoint : debug_info -> - identifier Pp.located message_token list -> unit + identifier Loc.located message_token list -> unit diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index e9a852455..91e1cd5ac 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -100,7 +100,7 @@ let print_rewrite_hintdb bas = Pptactic.pr_glob_tactic (Global.env()) h.rew_tac) (find_rewrites bas)) -type raw_rew_rule = loc * constr * bool * raw_tactic_expr +type raw_rew_rule = Loc.t * constr * bool * raw_tactic_expr (* Applies all the rules of one base *) let one_base general_rewrite_maybe_in tac_main bas = diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index e5ec949ed..6bd8e1536 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -12,7 +12,7 @@ open Tacmach open Equality (** Rewriting rules before tactic interpretation *) -type raw_rew_rule = Pp.loc * Term.constr * bool * Tacexpr.raw_tactic_expr +type raw_rew_rule = Loc.t * Term.constr * bool * Tacexpr.raw_tactic_expr (** To add rewriting rules to a base *) val add_rew_rules : string -> raw_rew_rule list -> unit @@ -56,6 +56,6 @@ type hypinfo = { } val find_applied_relation : bool -> - Pp.loc -> + Loc.t -> Environ.env -> Evd.evar_map -> Term.constr -> bool -> hypinfo diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index c8fe1a426..6557e52ab 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -37,7 +37,6 @@ open Pfedit open Command open Globnames open Evd -open Compat open Locus open Misctypes diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 76ee9ff68..a817efc33 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -23,7 +23,7 @@ open Misctypes let absurd c gls = let env = pf_env gls and sigma = project gls in - let _,j = Coercion.inh_coerce_to_sort dummy_loc env + let _,j = Coercion.inh_coerce_to_sort Loc.ghost env (Evd.create_goal_evar_defs sigma) (Retyping.get_judgment_of env sigma c) in let c = j.Environ.utj_val in (tclTHENS diff --git a/tactics/elim.mli b/tactics/elim.mli index fe19c0b24..ab2d4ad5e 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -20,7 +20,7 @@ val introElimAssumsThen : (branch_assumptions -> tactic) -> branch_args -> tactic val introCaseAssumsThen : - (intro_pattern_expr Pp.located list -> branch_assumptions -> tactic) -> + (intro_pattern_expr Loc.located list -> branch_assumptions -> tactic) -> branch_args -> tactic val general_decompose : (identifier * constr -> bool) -> constr -> tactic diff --git a/tactics/equality.ml b/tactics/equality.ml index 81457fc9c..f7e7361d5 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1147,7 +1147,7 @@ let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause = then ( (* Require Import Eqdec_dec copied from vernac_require in vernacentries.ml*) let qidl = qualid_of_reference - (Ident (dummy_loc,id_of_string "Eqdep_dec")) in + (Ident (Loc.ghost,id_of_string "Eqdep_dec")) in Library.require_library [qidl] (Some false); (* cut with the good equality and prove the requested goal *) tclTHENS (cut (mkApp (ceq,new_eq_args)) ) @@ -1170,7 +1170,7 @@ let injClause ipats with_evars = function | Some c -> onInductionArg (inj ipats with_evars) c let injConcl gls = injClause [] false None gls -let injHyp id gls = injClause [] false (Some (ElimOnIdent (dummy_loc,id))) gls +let injHyp id gls = injClause [] false (Some (ElimOnIdent (Loc.ghost,id))) gls let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause gls = let sort = pf_apply get_type_of gls (pf_concl gls) in diff --git a/tactics/equality.mli b/tactics/equality.mli index cd04181c0..c7ac34697 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -91,9 +91,9 @@ val discrHyp : identifier -> tactic val discrEverywhere : evars_flag -> tactic val discr_tac : evars_flag -> constr with_bindings induction_arg option -> tactic -val inj : intro_pattern_expr located list -> evars_flag -> +val inj : intro_pattern_expr Loc.located list -> evars_flag -> constr with_bindings -> tactic -val injClause : intro_pattern_expr located list -> evars_flag -> +val injClause : intro_pattern_expr Loc.located list -> evars_flag -> constr with_bindings induction_arg option -> tactic val injHyp : identifier -> tactic val injConcl : tactic diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index 4b5229010..1b5c2d6d0 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -52,7 +52,7 @@ let instantiate n (ist,rawc) ido gl = gl let let_evar name typ gls = - let src = (dummy_loc,Evar_kinds.GoalEvar) in + let src = (Loc.ghost,Evar_kinds.GoalEvar) in let sigma',evar = Evarutil.new_evar gls.sigma (pf_env gls) ~src typ in Refiner.tclTHEN (Refiner.tclEVARS sigma') (Tactics.letin_tac None name evar None Locusops.nowhere) gls diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index bff4f4760..7bfda9802 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -125,7 +125,7 @@ END type 'id gen_place= ('id * hyp_location_flag,unit) location -type loc_place = identifier Pp.located gen_place +type loc_place = identifier Loc.located gen_place type place = identifier gen_place let pr_gen_place pr_id = function @@ -167,11 +167,11 @@ ARGUMENT EXTEND hloc | [ "in" "|-" "*" ] -> [ ConclLocation () ] | [ "in" ident(id) ] -> - [ HypLocation ((Pp.dummy_loc,id),InHyp) ] + [ HypLocation ((Loc.ghost,id),InHyp) ] | [ "in" "(" "Type" "of" ident(id) ")" ] -> - [ HypLocation ((Pp.dummy_loc,id),InHypTypeOnly) ] + [ HypLocation ((Loc.ghost,id),InHypTypeOnly) ] | [ "in" "(" "Value" "of" ident(id) ")" ] -> - [ HypLocation ((Pp.dummy_loc,id),InHypValueOnly) ] + [ HypLocation ((Loc.ghost,id),InHypValueOnly) ] END diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index ee4f38c9d..60ee03f0e 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -33,7 +33,7 @@ val glob : constr_expr Pcoq.Gram.entry type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location -type loc_place = identifier Pp.located gen_place +type loc_place = identifier Loc.located gen_place type place = identifier gen_place val rawwit_hloc : loc_place raw_abstract_argument_type @@ -41,11 +41,11 @@ val wit_hloc : place typed_abstract_argument_type val hloc : loc_place Pcoq.Gram.entry val pr_hloc : loc_place -> Pp.std_ppcmds -val in_arg_hyp: (Names.identifier Pp.located list option * bool) Pcoq.Gram.entry -val globwit_in_arg_hyp : (Names.identifier Pp.located list option * bool) glob_abstract_argument_type -val rawwit_in_arg_hyp : (Names.identifier Pp.located list option * bool) raw_abstract_argument_type +val in_arg_hyp: (Names.identifier Loc.located list option * bool) Pcoq.Gram.entry +val globwit_in_arg_hyp : (Names.identifier Loc.located list option * bool) glob_abstract_argument_type +val rawwit_in_arg_hyp : (Names.identifier Loc.located list option * bool) raw_abstract_argument_type val wit_in_arg_hyp : (Names.identifier list option * bool) typed_abstract_argument_type -val raw_in_arg_hyp_to_clause : (Names.identifier Pp.located list option * bool) -> Locus.clause +val raw_in_arg_hyp_to_clause : (Names.identifier Loc.located list option * bool) -> Locus.clause val glob_in_arg_hyp_to_clause : (Names.identifier list option * bool) -> Locus.clause val pr_in_arg_hyp : (Names.identifier list option * bool) -> Pp.std_ppcmds diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 8abb9c9e4..c414339ff 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -22,7 +22,6 @@ open Errors open Util open Evd open Equality -open Compat open Misctypes (**********************************************************************) @@ -67,7 +66,7 @@ END let induction_arg_of_quantified_hyp = function | AnonHyp n -> ElimOnAnonHyp n - | NamedHyp id -> ElimOnIdent (Pp.dummy_loc,id) + | NamedHyp id -> ElimOnIdent (Loc.ghost,id) (* Versions *_main must come first!! so that "1" is interpreted as a ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a @@ -558,7 +557,7 @@ let subst_var_with_hole occ tid t = if !occref = 0 then x else (incr locref; - GHole (make_loc (!locref,0), + GHole (Loc.make_loc (!locref,0), Evar_kinds.QuestionMark(Evar_kinds.Define true)))) else x | c -> map_glob_constr_left_to_right substrec c in @@ -575,7 +574,7 @@ let subst_hole_with_term occ tc t = if !occref = 0 then tc else (incr locref; - GHole (make_loc (!locref,0), + GHole (Loc.make_loc (!locref,0), Evar_kinds.QuestionMark(Evar_kinds.Define true))) | c -> map_glob_constr_left_to_right substrec c in @@ -599,7 +598,7 @@ let hResolve id c occ t gl = Pretyping.understand sigma env t_hole with | Loc.Exc_located (loc,Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _)) -> - resolve_hole (subst_hole_with_term (fst (unloc loc)) c_raw t_hole) + resolve_hole (subst_hole_with_term (fst (Loc.unloc loc)) c_raw t_hole) in let t_constr = resolve_hole (subst_var_with_hole occ id t_raw) in let t_constr_type = Retyping.get_type_of env sigma t_constr in diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index d1d3d90c5..d5ee78fea 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -64,10 +64,10 @@ let h_generalize cl = let h_generalize_dep c = abstract_tactic (TacGeneralizeDep c) (generalize_dep c) let h_let_tac b na c cl = - let with_eq = if b then None else Some (true,(Pp.dummy_loc,IntroAnonymous)) in + let with_eq = if b then None else Some (true,(Loc.ghost,IntroAnonymous)) in abstract_tactic (TacLetTac (na,c,cl,b)) (letin_tac with_eq na c None cl) let h_let_pat_tac b na c cl = - let with_eq = if b then None else Some (true,(Pp.dummy_loc,IntroAnonymous)) in + let with_eq = if b then None else Some (true,(Loc.ghost,IntroAnonymous)) in abstract_tactic (TacLetTac (na,snd c,cl,b)) (letin_pat_tac with_eq na c None cl) @@ -132,8 +132,8 @@ let h_transitivity c = abstract_tactic (TacTransitivity c) (intros_transitivity c) -let h_simplest_apply c = h_apply false false [Pp.dummy_loc,(c,NoBindings)] -let h_simplest_eapply c = h_apply false true [Pp.dummy_loc,(c,NoBindings)] +let h_simplest_apply c = h_apply false false [Loc.ghost,(c,NoBindings)] +let h_simplest_eapply c = h_apply false true [Loc.ghost,(c,NoBindings)] let h_simplest_elim c = h_elim false (c,NoBindings) None let h_simplest_case c = h_case false (c,NoBindings) diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index af7a2061b..cffe84252 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Loc open Names open Pp open Term diff --git a/tactics/inv.mli b/tactics/inv.mli index 7dc9feb2c..05ba0e576 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Loc open Pp open Names open Term diff --git a/tactics/leminv.mli b/tactics/leminv.mli index fc72bd4e4..16e0b958f 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -1,3 +1,12 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Loc open Pp open Names open Term diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 867fea08c..180783983 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -39,7 +39,6 @@ open Command open Libnames open Globnames open Evd -open Compat open Misctypes open Locus open Locusops @@ -55,10 +54,10 @@ let init_setoid () = else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"] let proper_class = - lazy (class_info (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.Proper")))) + lazy (class_info (Nametab.global (Qualid (Loc.ghost, qualid_of_string "Coq.Classes.Morphisms.Proper")))) let proper_proxy_class = - lazy (class_info (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.ProperProxy")))) + lazy (class_info (Nametab.global (Qualid (Loc.ghost, qualid_of_string "Coq.Classes.Morphisms.ProperProxy")))) let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs)))) @@ -150,7 +149,7 @@ let build_signature evars env m (cstrs : (types * types option) option list) (finalcstr : (types * types option) option) = let new_evar evars env t = new_cstr_evar evars env - (* ~src:(dummy_loc, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t + (* ~src:(Loc.ghost, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t in let mk_relty evars env ty obj = match obj with @@ -1478,33 +1477,33 @@ TACTIC EXTEND GenRew [ cl_rewrite_clause_newtac_tac c o AllOccurrences None ] END -let mkappc s l = CAppExpl (dummy_loc,(None,(Libnames.Ident (dummy_loc,id_of_string s))),l) +let mkappc s l = CAppExpl (Loc.ghost,(None,(Libnames.Ident (Loc.ghost,id_of_string s))),l) let declare_an_instance n s args = - ((dummy_loc,Name n), Explicit, - CAppExpl (dummy_loc, (None, Qualid (dummy_loc, qualid_of_string s)), + ((Loc.ghost,Name n), Explicit, + CAppExpl (Loc.ghost, (None, Qualid (Loc.ghost, qualid_of_string s)), args)) let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance global binders instance fields = - new_instance binders instance (Some (CRecord (dummy_loc,None,fields))) + new_instance binders instance (Some (CRecord (Loc.ghost,None,fields))) ~global:(not (Locality.use_section_locality ())) ~generalize:false None let declare_instance_refl global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" in anew_instance global binders instance - [(Ident (dummy_loc,id_of_string "reflexivity"),lemma)] + [(Ident (Loc.ghost,id_of_string "reflexivity"),lemma)] let declare_instance_sym global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric" in anew_instance global binders instance - [(Ident (dummy_loc,id_of_string "symmetry"),lemma)] + [(Ident (Loc.ghost,id_of_string "symmetry"),lemma)] let declare_instance_trans global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive" in anew_instance global binders instance - [(Ident (dummy_loc,id_of_string "transitivity"),lemma)] + [(Ident (Loc.ghost,id_of_string "transitivity"),lemma)] let declare_relation ?(binders=[]) a aeq n refl symm trans = init_setoid (); @@ -1528,16 +1527,16 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in ignore( anew_instance global binders instance - [(Ident (dummy_loc,id_of_string "PreOrder_Reflexive"), lemma1); - (Ident (dummy_loc,id_of_string "PreOrder_Transitive"),lemma3)]) + [(Ident (Loc.ghost,id_of_string "PreOrder_Reflexive"), lemma1); + (Ident (Loc.ghost,id_of_string "PreOrder_Transitive"),lemma3)]) | (None, Some lemma2, Some lemma3) -> let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in ignore( anew_instance global binders instance - [(Ident (dummy_loc,id_of_string "PER_Symmetric"), lemma2); - (Ident (dummy_loc,id_of_string "PER_Transitive"),lemma3)]) + [(Ident (Loc.ghost,id_of_string "PER_Symmetric"), lemma2); + (Ident (Loc.ghost,id_of_string "PER_Transitive"),lemma3)]) | (Some lemma1, Some lemma2, Some lemma3) -> let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in @@ -1545,9 +1544,9 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in ignore( anew_instance global binders instance - [(Ident (dummy_loc,id_of_string "Equivalence_Reflexive"), lemma1); - (Ident (dummy_loc,id_of_string "Equivalence_Symmetric"), lemma2); - (Ident (dummy_loc,id_of_string "Equivalence_Transitive"), lemma3)]) + [(Ident (Loc.ghost,id_of_string "Equivalence_Reflexive"), lemma1); + (Ident (Loc.ghost,id_of_string "Equivalence_Symmetric"), lemma2); + (Ident (Loc.ghost,id_of_string "Equivalence_Transitive"), lemma3)]) type 'a binders_argtype = (local_binder list, 'a) Genarg.abstract_argument_type @@ -1626,7 +1625,7 @@ VERNAC COMMAND EXTEND AddParametricRelation3 [ declare_relation ~binders:b a aeq n None None (Some lemma3) ] END -let cHole = CHole (dummy_loc, None) +let cHole = CHole (Loc.ghost, None) open Entries open Libnames @@ -1723,9 +1722,9 @@ let add_setoid global binders a aeq t n = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in ignore( anew_instance global binders instance - [(Ident (dummy_loc,id_of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); - (Ident (dummy_loc,id_of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); - (Ident (dummy_loc,id_of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]) + [(Ident (Loc.ghost,id_of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); + (Ident (Loc.ghost,id_of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); + (Ident (Loc.ghost,id_of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]) let add_morphism_infer glob m n = init_setoid (); @@ -1754,13 +1753,13 @@ let add_morphism glob binders m s n = init_setoid (); let instance_id = add_suffix n "_Proper" in let instance = - ((dummy_loc,Name instance_id), Explicit, - CAppExpl (dummy_loc, - (None, Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper")), + ((Loc.ghost,Name instance_id), Explicit, + CAppExpl (Loc.ghost, + (None, Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper")), [cHole; s; m])) in let tac = Tacinterp.interp <:tactic<add_morphism_tactic>> in - ignore(new_instance ~global:glob binders instance (Some (CRecord (dummy_loc,None,[]))) + ignore(new_instance ~global:glob binders instance (Some (CRecord (Loc.ghost,None,[]))) ~generalize:false ~tac ~hook:(declare_projection n instance_id) None) VERNAC COMMAND EXTEND AddSetoid1 diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 45e48a9d7..2beba9888 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -51,7 +51,6 @@ open Syntax_def open Pretyping open Extrawit open Pcoq -open Compat open Evd open Misctypes open Miscops @@ -95,7 +94,7 @@ type value = | VList of value list | VRec of (identifier*value) list ref * glob_tactic_expr -let dloc = dummy_loc +let dloc = Loc.ghost let catch_error call_trace tac g = if call_trace = [] then tac g else try tac g with @@ -156,7 +155,7 @@ let ((tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t), let ((value_in : value -> Dyn.t), (value_out : Dyn.t -> value)) = Dyn.create "value" -let valueIn t = TacDynamic (dummy_loc,value_in t) +let valueIn t = TacDynamic (Loc.ghost,value_in t) let valueOut = function | TacDynamic (_,d) -> if (Dyn.tag d) = "value" then @@ -1547,14 +1546,14 @@ let interp_open_constr_with_bindings ist env sigma (c,bl) = sigma, (c, bl) let loc_of_bindings = function -| NoBindings -> dummy_loc +| NoBindings -> Loc.ghost | ImplicitBindings l -> loc_of_glob_constr (fst (list_last l)) | ExplicitBindings l -> pi1 (list_last l) let interp_open_constr_with_bindings_loc ist env sigma ((c,_),bl as cb) = let loc1 = loc_of_glob_constr c in let loc2 = loc_of_bindings bl in - let loc = if loc2 = dummy_loc then loc1 else join_loc loc1 loc2 in + let loc = if loc2 = Loc.ghost then loc1 else Loc.merge loc1 loc2 in let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in sigma, (loc,cb) diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index d1fe9de11..7ce0d3f84 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -104,7 +104,7 @@ val intern_constr_with_bindings : glob_constr_and_expr * glob_constr_and_expr bindings val intern_hyp : - glob_sign -> identifier Pp.located -> identifier Pp.located + glob_sign -> identifier Loc.located -> identifier Loc.located val subst_genarg : substitution -> glob_generic_argument -> glob_generic_argument @@ -129,7 +129,7 @@ val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map val interp_tac_gen : (identifier * value) list -> identifier list -> debug_info -> raw_tactic_expr -> tactic -val interp_hyp : interp_sign -> goal sigma -> identifier located -> identifier +val interp_hyp : interp_sign -> goal sigma -> identifier Loc.located -> identifier val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr bindings -> Evd.evar_map * constr bindings @@ -165,8 +165,8 @@ val print_ltac : Libnames.qualid -> std_ppcmds exception CannotCoerceTo of string -val interp_ltac_var : (value -> 'a) -> interp_sign -> Environ.env option -> identifier located -> 'a +val interp_ltac_var : (value -> 'a) -> interp_sign -> Environ.env option -> identifier Loc.located -> 'a -val interp_int : interp_sign -> identifier located -> int +val interp_int : interp_sign -> identifier Loc.located -> int -val error_ltac_variable : loc -> identifier -> Environ.env option -> value -> string -> 'a +val error_ltac_variable : Loc.t -> identifier -> Environ.env option -> value -> string -> 'a diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 4ba26dceb..664000797 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -174,7 +174,7 @@ type branch_args = { nassums : int; (* the number of assumptions to be introduced *) branchsign : bool list; (* the signature of the branch. true=recursive argument, false=constant *) - branchnames : intro_pattern_expr located list} + branchnames : intro_pattern_expr Loc.located list} type branch_assumptions = { ba : branch_args; (* the branch args *) diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 3c1beda40..d369109ed 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Loc open Pp open Names open Term @@ -126,7 +127,7 @@ type branch_assumptions = { (** [check_disjunctive_pattern_size loc pats n] returns an appropriate error message if |pats| <> n *) val check_or_and_pattern_size : - Pp.loc -> or_and_intro_pattern_expr -> int -> unit + Loc.t -> or_and_intro_pattern_expr -> int -> unit (** Tolerate "[]" to mean a disjunctive pattern of any length *) val fix_empty_or_and_pattern : int -> or_and_intro_pattern_expr -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2f386def1..0d32ed46f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Compat open Pp open Errors open Util @@ -61,7 +60,7 @@ let rec nb_prod x = let inj_with_occurrences e = (AllOccurrences,e) -let dloc = dummy_loc +let dloc = Loc.ghost let typ_of = Retyping.get_type_of diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 2cbefb817..6cdac9d55 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Loc open Pp open Names open Term diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 61bc1ae7c..57987ef41 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -59,7 +59,7 @@ exception InductiveWithSort exception ParameterWithoutEquality of constant exception NonSingletonProp of inductive -let dl = dummy_loc +let dl = Loc.ghost (* Some pre declaration of constant we are going to use *) let bb = constr_of_global Coqlib.glob_bool diff --git a/toplevel/backtrack.mli b/toplevel/backtrack.mli index f6c69d890..bfd3c47a0 100644 --- a/toplevel/backtrack.mli +++ b/toplevel/backtrack.mli @@ -61,7 +61,7 @@ val reset_initial : unit -> unit (** Reset to the last known state just before defining [id] *) -val reset_name : Names.identifier Pp.located -> unit +val reset_name : Names.identifier Loc.located -> unit (** When a proof is ended (via either Qed/Admitted/Restart/Abort), old proof steps should be marked differently to avoid jumping back diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 281ae784e..849bd7ce2 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Compat open Pp open Errors open Util @@ -16,10 +15,10 @@ open Pretype_errors open Indrec let print_loc loc = - if loc = dummy_loc then + if loc = Loc.ghost then (str"<unknown>") else - let loc = unloc loc in + let loc = Loc.unloc loc in (int (fst loc) ++ str"-" ++ int (snd loc)) let guill s = "\""^s^"\"" @@ -43,7 +42,7 @@ let explain_exn_default = function | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.") (* Meta-exceptions *) | Loc.Exc_located (loc,exc) -> - hov 0 ((if loc = dummy_loc then (mt ()) + hov 0 ((if loc = Loc.ghost then (mt ()) else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) ++ Errors.print_no_anomaly exc) | EvaluatedError (msg,None) -> msg diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli index 75d742ce1..9a50da747 100644 --- a/toplevel/cerrors.mli +++ b/toplevel/cerrors.mli @@ -8,7 +8,7 @@ (** Error report. *) -val print_loc : Pp.loc -> Pp.std_ppcmds +val print_loc : Loc.t -> Pp.std_ppcmds (** Pre-explain a vernac interpretation error *) diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 31a02758f..fa2f2e168 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -69,7 +69,7 @@ let existing_instance glob g = let mismatched_params env n m = mismatched_ctx_inst env Parameters n m let mismatched_props env n m = mismatched_ctx_inst env Properties n m -type binder_list = (identifier located * bool * constr_expr) list +type binder_list = (identifier Loc.located * bool * constr_expr) list (* Declare everything in the parameters as implicit, and the class instance as well *) @@ -135,13 +135,13 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props (fun avoid (clname, (id, _, t)) -> match clname with | Some (cl, b) -> - let t = CHole (Pp.dummy_loc, None) in + let t = CHole (Loc.ghost, None) in t, avoid | None -> failwith ("new instance: under-applied typeclass")) cl | Explicit -> cl, Idset.empty in - let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in + let tclass = if generalize then CGeneralization (Loc.ghost, Implicit, Some AbsPi, tclass) else tclass in let k, cty, ctx', ctx, len, imps, subst = let impls, ((env', ctx), imps) = interp_context_evars evars env ctx in let c', imps' = interp_type_evars_impls ~impls ~evdref:evars ~fail_evar:false env' tclass in @@ -232,7 +232,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props k.cl_projs; c :: props, rest' with Not_found -> - (CHole (Pp.dummy_loc, Some Evar_kinds.GoalEvar) :: props), rest + (CHole (Loc.ghost, Some Evar_kinds.GoalEvar) :: props), rest else props, rest) ([], props) k.cl_props in @@ -348,6 +348,6 @@ let context l = match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls in Command.declare_assumption false (Local (* global *), Definitional) t - [] impl (* implicit *) None (* inline *) (dummy_loc, id)) + [] impl (* implicit *) None (* inline *) (Loc.ghost, id)) in List.iter fn (List.rev ctx) diff --git a/toplevel/command.ml b/toplevel/command.ml index 3d97e544e..e8e651618 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -355,7 +355,7 @@ let extract_params indl = let extract_inductive indl = List.map (fun ((_,indname),_,ar,lc) -> { ind_name = indname; - ind_arity = Option.cata (fun x -> x) (CSort (dummy_loc,GType None)) ar; + ind_arity = Option.cata (fun x -> x) (CSort (Loc.ghost,GType None)) ar; ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc }) indl @@ -481,7 +481,7 @@ let check_mutuality env isfix fixl = type structured_fixpoint_expr = { fix_name : identifier; - fix_annot : identifier located option; + fix_annot : identifier Loc.located option; fix_binders : local_binder list; fix_body : constr_expr option; fix_type : constr_expr @@ -563,7 +563,7 @@ let mkSubset name typ prop = [| typ; mkLambda (name, typ, prop) |]) let sigT = Lazy.lazy_from_fun build_sigma_type -let make_qref s = Qualid (dummy_loc, qualid_of_string s) +let make_qref s = Qualid (Loc.ghost, qualid_of_string s) let lt_ref = make_qref "Init.Peano.lt" let rec telescope = function @@ -687,7 +687,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = mkApp (constr_of_global (delayed_force fix_sub_ref), [| argtyp ; wf_rel ; Evarutil.e_new_evar isevars env - ~src:(dummy_loc, Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof; + ~src:(Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof; prop ; intern_body_lam |]) in let _ = isevars := Evarutil.nf_evar_map !isevars in @@ -807,7 +807,7 @@ let declare_fixpoint ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns = (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in - let indexes = search_guard dummy_loc (Global.env()) indexes fixdecls in + let indexes = search_guard Loc.ghost (Global.env()) indexes fixdecls in let fiximps = List.map (fun (n,r,p) -> r) fiximps in let fixdecls = list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in @@ -915,7 +915,7 @@ let do_program_recursive fixkind fixl ntns = Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs) in let indexes = - Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in + Pretyping.search_guard Loc.ghost (Global.env ()) possible_indexes fixdecls in list_iter_i (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) fixl end; Obligations.add_mutual_definitions defs ntns fixkind diff --git a/toplevel/command.mli b/toplevel/command.mli index a43f2ad37..c4b0dba8a 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -49,9 +49,9 @@ val interp_assumption : val declare_assumption : coercion_flag -> assumption_kind -> types -> Impargs.manual_implicits -> - bool (** implicit *) -> Entries.inline -> variable located -> unit + bool (** implicit *) -> Entries.inline -> variable Loc.located -> unit -val declare_assumptions : variable located list -> +val declare_assumptions : variable Loc.located list -> coercion_flag -> assumption_kind -> types -> Impargs.manual_implicits -> bool -> Entries.inline -> unit @@ -99,7 +99,7 @@ val do_mutual_inductive : type structured_fixpoint_expr = { fix_name : identifier; - fix_annot : identifier located option; + fix_annot : identifier Loc.located option; fix_binders : local_binder list; fix_body : constr_expr option; fix_type : constr_expr diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index e0923cda0..be8fbf89d 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1002,12 +1002,12 @@ let explain_ltac_call_trace (nrep,last,trace,loc) = Pptactic.pr_glob_tactic (Global.env()) t ++ str ")" | Proof_type.LtacAtomCall (te,otac) -> quote (Pptactic.pr_glob_tactic (Global.env()) - (Tacexpr.TacAtom (dummy_loc,te))) + (Tacexpr.TacAtom (Loc.ghost,te))) ++ (match !otac with | Some te' when (Obj.magic te' <> te) -> strbrk " (expanded to " ++ quote (Pptactic.pr_tactic (Global.env()) - (Tacexpr.TacAtom (dummy_loc,te'))) + (Tacexpr.TacAtom (Loc.ghost,te'))) ++ str ")" | _ -> mt ()) | Proof_type.LtacConstrInterp (c,(vars,unboundvars)) -> diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index 7607bda42..b2f105926 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -38,7 +38,7 @@ val explain_reduction_tactic_error : Tacred.reduction_tactic_error -> std_ppcmds val explain_ltac_call_trace : - int * Proof_type.ltac_call_kind * Proof_type.ltac_trace * Pp.loc -> + int * Proof_type.ltac_call_kind * Proof_type.ltac_trace * Loc.t -> std_ppcmds val explain_module_error : Modops.module_typing_error -> std_ppcmds diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 5ffbedcd7..b7a6af494 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -8,7 +8,6 @@ open Vernacexpr open Names -open Compat open Errors open Util open Pp @@ -366,8 +365,8 @@ let eval_call c = | Errors.Quit -> None, "Quit is not allowed by coqide!" | Vernac.DuringCommandInterp (_,inner) -> handle_exn inner | Error_in_file (_,_,inner) -> None, pr_exn inner - | Loc.Exc_located (loc, inner) when loc = dummy_loc -> None, pr_exn inner - | Loc.Exc_located (loc, inner) -> Some (Pp.unloc loc), pr_exn inner + | Loc.Exc_located (loc, inner) when loc = Loc.ghost -> None, pr_exn inner + | Loc.Exc_located (loc, inner) -> Some (Loc.unloc loc), pr_exn inner | e -> None, pr_exn e in let interruptible f x = diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index dc3e0dc47..f9e58a432 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -334,7 +334,7 @@ requested | InType -> recs ^ "t_nodep") ) in let newid = add_suffix (basename_of_global (IndRef ind)) suffix in - let newref = (dummy_loc,newid) in + let newref = (Loc.ghost,newid) in ((newref,isdep,ind,z)::l1),l2 in match t with diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli index 5a4dbabb6..74b8890ec 100644 --- a/toplevel/indschemes.mli +++ b/toplevel/indschemes.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Loc open Pp open Names open Term diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 31f5d2994..c2891e0c1 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -56,7 +56,7 @@ let adjust_guardness_conditions const = function lemma_guard (Array.to_list fixdefs) in *) let indexes = - search_guard dummy_loc (Global.env()) possible_indexes fixdecls in + search_guard Loc.ghost (Global.env()) possible_indexes fixdecls in { const with const_entry_body = mkFix ((indexes,0),fixdecls) } | c -> const diff --git a/toplevel/locality.mli b/toplevel/locality.mli index 5e8d45d87..6c2194cfe 100644 --- a/toplevel/locality.mli +++ b/toplevel/locality.mli @@ -8,7 +8,7 @@ (** * Managing locality *) -val locality_flag : (Pp.loc * bool) option ref +val locality_flag : (Loc.t * bool) option ref val check_locality : unit -> unit (** * Extracting the locality flag *) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index fe1cd7eb3..fee4fef18 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -1144,7 +1144,7 @@ let add_notation local c ((loc,df),modifiers) sc = (* Infix notations *) -let inject_var x = CRef (Ident (dummy_loc, id_of_string x)) +let inject_var x = CRef (Ident (Loc.ghost, id_of_string x)) let add_infix local ((loc,inf),modifiers) pr sc = check_infix_modifiers modifiers; diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 1b1c61a08..0d6bc39f3 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -13,7 +13,6 @@ open Util open Evd open Declare open Proof_type -open Compat (** - Get types of existentials ; @@ -61,7 +60,7 @@ type oblinfo = ev_hyps: named_context; ev_status: Evar_kinds.obligation_definition_status; ev_chop: int option; - ev_src: Evar_kinds.t located; + ev_src: Evar_kinds.t Loc.located; ev_typ: types; ev_tac: tactic option; ev_deps: Intset.t } @@ -313,13 +312,13 @@ let explain_no_obligations = function | None -> str "No obligations remaining" type obligation_info = - (Names.identifier * Term.types * Evar_kinds.t located * + (Names.identifier * Term.types * Evar_kinds.t Loc.located * Evar_kinds.obligation_definition_status * Intset.t * tactic option) array type obligation = { obl_name : identifier; obl_type : types; - obl_location : Evar_kinds.t located; + obl_location : Evar_kinds.t Loc.located; obl_body : constr option; obl_status : Evar_kinds.obligation_definition_status; obl_deps : Intset.t; @@ -329,7 +328,7 @@ type obligation = type obligations = (obligation array * int) type fixpoint_kind = - | IsFixpoint of (identifier located option * Constrexpr.recursion_order_expr) list + | IsFixpoint of (identifier Loc.located option * Constrexpr.recursion_order_expr) list | IsCoFixpoint type notations = (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list @@ -584,7 +583,7 @@ let declare_mutual_definition l = | IsFixpoint wfl -> let possible_indexes = list_map3 compute_possible_guardness_evidences wfl fixdefs fixtypes in - let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in + let indexes = Pretyping.search_guard Loc.ghost (Global.env ()) possible_indexes fixdecls in Some indexes, list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 l | IsCoFixpoint -> None, list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l @@ -628,7 +627,7 @@ let init_prog_info n b t deps fixkind notations obls impls kind reduce hook = assert(obls = [||]); let n = Nameops.add_suffix n "_obligation" in [| { obl_name = n; obl_body = None; - obl_location = dummy_loc, Evar_kinds.InternalHole; obl_type = t; + obl_location = Loc.ghost, Evar_kinds.InternalHole; obl_type = t; obl_status = Evar_kinds.Expand; obl_deps = Intset.empty; obl_tac = None } |], mkVar n diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli index 26e987974..a867a9372 100644 --- a/toplevel/obligations.mli +++ b/toplevel/obligations.mli @@ -40,7 +40,7 @@ val sort_dependencies : (int * evar_info * Intset.t) list -> (int * evar_info * evars contexts, object and type *) val eterm_obligations : env -> identifier -> evar_map -> int -> ?status:Evar_kinds.obligation_definition_status -> constr -> types -> - (identifier * types * Evar_kinds.t located * Evar_kinds.obligation_definition_status * Intset.t * + (identifier * types * Evar_kinds.t Loc.located * Evar_kinds.obligation_definition_status * Intset.t * tactic option) array (* Existential key, obl. name, type as product, location of the original evar, associated tactic, @@ -52,7 +52,7 @@ val eterm_obligations : env -> identifier -> evar_map -> int -> translation from obligation identifiers to constrs, new term, new type *) type obligation_info = - (identifier * Term.types * Evar_kinds.t located * + (identifier * Term.types * Evar_kinds.t Loc.located * Evar_kinds.obligation_definition_status * Intset.t * tactic option) array (* ident, type, location, (opaque or transparent, expand or define), dependencies, tactic to solve it *) @@ -80,7 +80,7 @@ type notations = (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list type fixpoint_kind = - | IsFixpoint of (identifier located option * Constrexpr.recursion_order_expr) list + | IsFixpoint of (identifier Loc.located option * Constrexpr.recursion_order_expr) list | IsCoFixpoint val add_mutual_definitions : diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 7991d0e58..feaa8c970 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -13,7 +13,6 @@ open Flags open Cerrors open Vernac open Pcoq -open Compat (* A buffer for the character read from a channel. We store the command * entered to be able to report errors without pretty-printing. *) @@ -124,7 +123,7 @@ let blanch_utf8_string s bp ep = String.sub s' 0 !j let print_highlight_location ib loc = - let (bp,ep) = unloc loc in + let (bp,ep) = Loc.unloc loc in let bp = bp - ib.start and ep = ep - ib.start in let highlight_lines = @@ -146,7 +145,7 @@ let print_highlight_location ib loc = str sn ++ str dn) in (l1 ++ li ++ ln) in - let loc = make_loc (bp,ep) in + let loc = Loc.make_loc (bp,ep) in (str"Toplevel input, characters " ++ Cerrors.print_loc loc ++ str":" ++ fnl () ++ highlight_lines ++ fnl ()) @@ -154,7 +153,7 @@ let print_highlight_location ib loc = let print_location_in_file s inlibrary fname loc = let errstrm = str"Error while reading " ++ str s in - if loc = dummy_loc then + if loc = Loc.ghost then hov 1 (errstrm ++ spc() ++ str" (unknown location):") ++ fnl () else let errstrm = @@ -163,7 +162,7 @@ let print_location_in_file s inlibrary fname loc = hov 0 (errstrm ++ str"Module " ++ str ("\""^fname^"\"") ++ spc() ++ str"characters " ++ Cerrors.print_loc loc) ++ fnl () else - let (bp,ep) = unloc loc in + let (bp,ep) = Loc.unloc loc in let ic = open_in fname in let rec line_of_pos lin bol cnt = if cnt < bp then @@ -178,7 +177,7 @@ let print_location_in_file s inlibrary fname loc = hov 0 (* No line break so as to follow emacs error message format *) (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++ str", line " ++ int line ++ str", characters " ++ - Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":" ++ + Cerrors.print_loc (Loc.make_loc (bp-bol,ep-bol))) ++ str":" ++ fnl () with e -> (close_in ic; @@ -192,15 +191,15 @@ let print_command_location ib dloc = | None -> (mt ()) let valid_loc dloc loc = - loc <> dummy_loc + loc <> Loc.ghost & match dloc with | Some dloc -> - let (bd,ed) = unloc dloc in let (b,e) = unloc loc in bd<=b & e<=ed + let (bd,ed) = Loc.unloc dloc in let (b,e) = Loc.unloc loc in bd<=b & e<=ed | _ -> true let valid_buffer_loc ib dloc loc = valid_loc dloc loc & - let (b,e) = unloc loc in b-ib.start >= 0 & e-ib.start < ib.len & b<=e + let (b,e) = Loc.unloc loc in b-ib.start >= 0 & e-ib.start < ib.len & b<=e (*s The Coq prompt is the name of the focused proof, if any, and "Coq" otherwise. We trap all exceptions to prevent the error message printing @@ -283,7 +282,7 @@ let print_toplevel_error exc = let (dloc,exc) = match exc with | DuringCommandInterp (loc,ie) -> - if loc = dummy_loc then (None,ie) else (Some loc, ie) + if loc = Loc.ghost then (None,ie) else (Some loc, ie) | _ -> (None, exc) in let (locstrm,exc) = @@ -312,7 +311,7 @@ let print_toplevel_error exc = (* Read the input stream until a dot is encountered *) let parse_to_dot = - let rec dot st = match get_tok (Stream.next st) with + let rec dot st = match Compat.get_tok (Stream.next st) with | Tok.KEYWORD "." -> () | Tok.EOI -> raise End_of_input | _ -> dot st diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index ac3dd39cb..a1015d15e 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -17,13 +17,12 @@ open System open Vernacexpr open Vernacinterp open Ppvernac -open Compat (* The functions in this module may raise (unexplainable!) exceptions. Use the module Coqtoplevel, which catches these exceptions (the exceptions are explained only at the toplevel). *) -exception DuringCommandInterp of Pp.loc * exn +exception DuringCommandInterp of Loc.t * exn exception HasNotFailed @@ -51,13 +50,13 @@ let raise_with_file file exc = let (cmdloc,re) = match exc with | DuringCommandInterp(loc,e) -> (loc,e) - | e -> (dummy_loc,e) + | e -> (Loc.ghost,e) in let (inner,inex) = match re with - | Error_in_file (_, (b,f,loc), e) when loc <> dummy_loc -> + | Error_in_file (_, (b,f,loc), e) when loc <> Loc.ghost -> ((b, f, loc), e) - | Loc.Exc_located (loc, e) when loc <> dummy_loc -> + | Loc.Exc_located (loc, e) when loc <> Loc.ghost -> ((false,file, loc), e) | Loc.Exc_located (_, e) | e -> ((false,file,cmdloc), e) in @@ -152,7 +151,7 @@ let close_input in_chan (_,verb) = with _ -> () let verbose_phrase verbch loc = - let loc = unloc loc in + let loc = Loc.unloc loc in match verbch with | Some ch -> let len = snd loc - fst loc in @@ -184,7 +183,7 @@ let set_formatter_translator() = Format.set_max_boxes max_int let pr_new_syntax loc ocom = - let loc = unloc loc in + let loc = Loc.unloc loc in if !beautify_file then set_formatter_translator(); let fs = States.freeze () in let com = match ocom with @@ -308,10 +307,10 @@ and read_vernac_file verbosely s = close_input in_chan input; (* we must close the file first *) match real_error e with | End_of_input -> - if do_beautify () then pr_new_syntax (make_loc (max_int,max_int)) None + if do_beautify () then pr_new_syntax (Loc.make_loc (max_int,max_int)) None | _ -> raise_with_file fname e -(** [eval_expr : ?preserving:bool -> Pp.loc * Vernacexpr.vernac_expr -> unit] +(** [eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit] It executes one vernacular command. By default the command is considered as non-state-preserving, in which case we add it to the Backtrack stack (triggering a save of a frozen state and the generation diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index 79ea1a4c5..924f2a65e 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -12,12 +12,12 @@ Raises [End_of_file] if EOF (or Ctrl-D) is reached. *) val parse_sentence : Pcoq.Gram.parsable * in_channel option -> - Pp.loc * Vernacexpr.vernac_expr + Loc.t * Vernacexpr.vernac_expr (** Reads and executes vernac commands from a stream. The boolean [just_parsing] disables interpretation of commands. *) -exception DuringCommandInterp of Pp.loc * exn +exception DuringCommandInterp of Loc.t * exn exception End_of_input val just_parsing : bool ref @@ -28,7 +28,7 @@ val just_parsing : bool ref of a new state label). An example of state-preserving command is one coming from the query panel of Coqide. *) -val eval_expr : ?preserving:bool -> Pp.loc * Vernacexpr.vernac_expr -> unit +val eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit val raw_do_vernac : Pcoq.Gram.parsable -> unit (** Set XML hooks *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 16cf388b9..da30513c4 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -475,7 +475,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast = in Dumpglob.dump_moddef loc mp "mod"; if_verbose msg_info (str ("Module "^ string_of_id id ^" is declared")); - Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export + Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = (* We check the state of the system (in section, in module type) @@ -499,7 +499,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = List.iter (fun (export,id) -> Option.iter - (fun export -> vernac_import export [Ident (dummy_loc,id)]) export + (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export ) argsexport | _::_ -> let binders_ast = List.map @@ -517,7 +517,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = Dumpglob.dump_moddef loc mp "mod"; if_verbose msg_info (str ("Module "^ string_of_id id ^" is defined")); - Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) + Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export let vernac_end_module export (loc,id as lid) = @@ -547,7 +547,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = List.iter (fun (export,id) -> Option.iter - (fun export -> vernac_import export [Ident (dummy_loc,id)]) export + (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export ) argsexport | _ :: _ -> @@ -1172,7 +1172,7 @@ let vernac_check_may_eval redexp glopt rc = Evarutil.check_evars env sigma sigma' c; Arguments_renaming.rename_typing env c with P.PretypeError (_,_,P.UnsolvableImplicit _) - | Compat.Loc.Exc_located (_,P.PretypeError (_,_,P.UnsolvableImplicit _)) -> + | Loc.Exc_located (_,P.PretypeError (_,_,P.UnsolvableImplicit _)) -> Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) in match redexp with | None -> @@ -1265,7 +1265,7 @@ let interp_search_about_item = function | SearchString (s,sc) -> try let ref = - Notation.interp_notation_as_global_reference dummy_loc + Notation.interp_notation_as_global_reference Loc.ghost (fun _ -> true) s sc in GlobSearchSubPattern (Pattern.PRef ref) with UserError _ -> |