diff options
Diffstat (limited to 'plugins/ltac/extraargs.ml4')
| -rw-r--r-- | plugins/ltac/extraargs.ml4 | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index bb01aca558..702b830342 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -1,13 +1,13 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Pp open Genarg open Stdarg @@ -83,7 +83,7 @@ let pr_int_list_full _prc _prlc _prt l = pr_int_list l let pr_occurrences _prc _prlc _prt l = match l with | ArgArg x -> pr_int_list x - | ArgVar (loc, id) -> Id.print id + | ArgVar { CAst.loc = loc; v=id } -> Id.print id let occurrences_of = function | [] -> NoOccurrences @@ -104,7 +104,7 @@ let int_list_of_VList v = match Value.to_list v with let interp_occs ist gl l = match l with | ArgArg x -> x - | ArgVar (_,id as locid) -> + | ArgVar ({ CAst.v = id } as locid) -> (try int_list_of_VList (Id.Map.find id ist.lfun) with Not_found | CannotCoerceTo _ -> [interp_int ist locid]) let interp_occs ist gl l = @@ -190,7 +190,7 @@ END type 'id gen_place= ('id * hyp_location_flag,unit) location -type loc_place = Id.t Loc.located gen_place +type loc_place = lident gen_place type place = Id.t gen_place let pr_gen_place pr_id = function @@ -201,7 +201,7 @@ let pr_gen_place pr_id = function | HypLocation (id,InHypValueOnly) -> str "in (Value of " ++ pr_id id ++ str ")" -let pr_loc_place _ _ _ = pr_gen_place (fun (_,id) -> Id.print id) +let pr_loc_place _ _ _ = pr_gen_place (fun { CAst.v = id } -> Id.print id) let pr_place _ _ _ = pr_gen_place Id.print let pr_hloc = pr_loc_place () () () @@ -230,11 +230,11 @@ ARGUMENT EXTEND hloc | [ "in" "|-" "*" ] -> [ ConclLocation () ] | [ "in" ident(id) ] -> - [ HypLocation ((Loc.tag id),InHyp) ] + [ HypLocation ((CAst.make id),InHyp) ] | [ "in" "(" "Type" "of" ident(id) ")" ] -> - [ HypLocation ((Loc.tag id),InHypTypeOnly) ] + [ HypLocation ((CAst.make id),InHypTypeOnly) ] | [ "in" "(" "Value" "of" ident(id) ")" ] -> - [ HypLocation ((Loc.tag id),InHypValueOnly) ] + [ HypLocation ((CAst.make id),InHypValueOnly) ] END |