aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/funind/glob_term_to_relation.ml18
-rw-r--r--plugins/funind/indfun.ml52
-rw-r--r--plugins/ltac/coretactics.ml42
-rw-r--r--plugins/ltac/extraargs.ml414
-rw-r--r--plugins/ltac/extraargs.mli8
-rw-r--r--plugins/ltac/extratactics.ml42
-rw-r--r--plugins/ltac/g_ltac.ml422
-rw-r--r--plugins/ltac/g_tactic.ml461
-rw-r--r--plugins/ltac/pltac.mli7
-rw-r--r--plugins/ltac/pptactic.ml28
-rw-r--r--plugins/ltac/rewrite.ml4
-rw-r--r--plugins/ltac/tacentries.ml6
-rw-r--r--plugins/ltac/tacexpr.mli16
-rw-r--r--plugins/ltac/tacintern.ml44
-rw-r--r--plugins/ltac/tacintern.mli2
-rw-r--r--plugins/ltac/tacinterp.ml73
-rw-r--r--plugins/ltac/tacinterp.mli6
-rw-r--r--plugins/ltac/tactic_debug.mli2
-rw-r--r--plugins/ltac/tactic_matching.ml4
-rw-r--r--plugins/ltac/tauto.ml6
-rw-r--r--plugins/quote/g_quote.ml42
-rw-r--r--plugins/setoid_ring/newring.ml6
-rw-r--r--plugins/ssr/ssrcommon.ml8
-rw-r--r--plugins/ssr/ssrparser.ml460
-rw-r--r--plugins/ssr/ssrvernac.ml424
-rw-r--r--plugins/ssrmatching/ssrmatching.ml44
26 files changed, 250 insertions, 231 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 693ab464d..22881c32c 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1295,7 +1295,7 @@ let rec rebuild_return_type rt =
CAst.make ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t')
| Constrexpr.CLetIn(na,v,t,t') ->
CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t')
- | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([Loc.tag Anonymous],
+ | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([CAst.make Anonymous],
Constrexpr.Default Decl_kinds.Explicit, rt)],
CAst.make @@ Constrexpr.CSort(GType []))
@@ -1351,12 +1351,12 @@ let do_build_inductive
(fun (n,t,typ) acc ->
match typ with
| Some typ ->
- CAst.make @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
+ CAst.make @@ Constrexpr.CLetIn((CAst.make n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ),
acc)
| None ->
CAst.make @@ Constrexpr.CProdN
- ([Constrexpr.CLocalAssum([(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)],
+ ([Constrexpr.CLocalAssum([CAst.make n],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)],
acc
)
)
@@ -1418,12 +1418,12 @@ let do_build_inductive
(fun (n,t,typ) acc ->
match typ with
| Some typ ->
- CAst.make @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
+ CAst.make @@ Constrexpr.CLetIn((CAst.make n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ),
acc)
| None ->
CAst.make @@ Constrexpr.CProdN
- ([Constrexpr.CLocalAssum([(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)],
+ ([Constrexpr.CLocalAssum([CAst.make n],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)],
acc
)
)
@@ -1450,18 +1450,18 @@ let do_build_inductive
(fun (n,t,typ) ->
match typ with
| Some typ ->
- Constrexpr.CLocalDef((Loc.tag n), Constrextern.extern_glob_constr Id.Set.empty t,
+ Constrexpr.CLocalDef((CAst.make n), Constrextern.extern_glob_constr Id.Set.empty t,
Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ))
| None ->
Constrexpr.CLocalAssum
- ([(Loc.tag n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t)
+ ([(CAst.make n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t)
)
rels_params
in
let ext_rels_constructors =
Array.map (List.map
(fun (id,t) ->
- false,((Loc.tag id),
+ false,((CAst.make id),
with_full_print
(Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) (alpha_rt rel_params_ids t))
)
@@ -1469,7 +1469,7 @@ let do_build_inductive
(rel_constructors)
in
let rel_ind i ext_rel_constructors =
- (((Loc.tag @@ relnames.(i)), None),
+ (((CAst.make @@ relnames.(i)), None),
rel_params,
Some rel_arities.(i),
ext_rel_constructors),[]
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 96e4a94d3..e19fc9b62 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -155,7 +155,7 @@ let build_newrecursive
let sigma = Evd.from_env env0 in
let (rec_sign,rec_impls) =
List.fold_left
- (fun (env,impls) (((_,recname),_),bl,arityc,_) ->
+ (fun (env,impls) (({CAst.v=recname},_),bl,arityc,_) ->
let arityc = Constrexpr_ops.mkCProdN bl arityc in
let arity,ctx = Constrintern.interp_type env0 sigma arityc in
let evd = Evd.from_env env0 in
@@ -344,7 +344,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs interactive_proof
(continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int ->
Tacmach.tactic) : unit =
- let names = List.map (function (((_, name),_),_,_,_,_),_ -> name) fix_rec_l in
+ let names = List.map (function (({CAst.v=name},_),_,_,_,_),_ -> name) fix_rec_l in
let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in
let funs_args = List.map fst fun_bodies in
let funs_types = List.map (function ((_,_,_,types,_),_) -> types) fix_rec_l in
@@ -365,7 +365,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
f_R_mut)
in
let fname_kn (((fname,_),_,_,_,_),_) =
- let f_ref = Ident fname in
+ let f_ref = Ident CAst.(with_loc_val (fun ?loc n -> (loc,n)) fname) in
locate_with_msg
(pr_reference f_ref++str ": Not an inductive type!")
locate_constant
@@ -404,7 +404,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
match fixpoint_exprl with
- | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec ->
+ | [(({CAst.v=fname},pl),_,bl,ret_type,body),_] when not is_rec ->
let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in
ComDefinition.do_definition
~program_mode:false
@@ -413,7 +413,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ()));
let evd,rev_pconstants =
List.fold_left
- (fun (evd,l) ((((_,fname),_),_,_,_,_),_) ->
+ (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
let evd,c =
Evd.fresh_global
(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
@@ -430,7 +430,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
ComFixpoint.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
let evd,rev_pconstants =
List.fold_left
- (fun (evd,l) ((((_,fname),_),_,_,_,_),_) ->
+ (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
let evd,c =
Evd.fresh_global
(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
@@ -460,7 +460,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
let rec_arg_num =
let names =
List.map
- snd
+ CAst.(with_val (fun x -> x))
(Constrexpr_ops.names_of_local_assums args)
in
match wf_arg with
@@ -476,8 +476,8 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
(None,(Ident (Loc.tag fname)),None) ,
(List.map
(function
- | _,Anonymous -> assert false
- | _,Name e -> (Constrexpr_ops.mkIdentC e)
+ | {CAst.v=Anonymous} -> assert false
+ | {CAst.v=Name e} -> (Constrexpr_ops.mkIdentC e)
)
(Constrexpr_ops.names_of_local_assums args)
)
@@ -515,7 +515,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
| None ->
begin
match args with
- | [Constrexpr.CLocalAssum ([(_,Name x)],k,t)] -> t,x
+ | [Constrexpr.CLocalAssum ([{CAst.v=Name x}],k,t)] -> t,x
| _ -> error "Recursive argument must be specified"
end
| Some wf_args ->
@@ -525,7 +525,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
(function
| Constrexpr.CLocalAssum(l,k,t) ->
List.exists
- (function (_,Name id) -> Id.equal id wf_args | _ -> false)
+ (function {CAst.v=Name id} -> Id.equal id wf_args | _ -> false)
l
| _ -> false
)
@@ -546,7 +546,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
let fun_from_mes =
let applied_mes =
Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg]) in
- Constrexpr_ops.mkLambdaC ([(Loc.tag @@ Name wf_arg)],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes)
+ Constrexpr_ops.mkLambdaC ([CAst.make @@ 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])
@@ -557,7 +557,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(
- [Loc.tag @@ Name a;Loc.tag @@ Name b],
+ [CAst.make @@ Name a; CAst.make @@ Name b],
Constrexpr.Default Explicit,
wf_arg_type,
Constrexpr_ops.mkAppC(wf_rel_expr,
@@ -592,7 +592,7 @@ and rebuild_nal aux bk bl' nal typ =
| _,{ CAst.v = CProdN([],typ) } -> rebuild_nal aux bk bl' nal typ
| [], _ -> rebuild_bl aux bl' typ
| na::nal,{ CAst.v = CProdN(CLocalAssum(na'::nal',bk',nal't)::rest,typ') } ->
- if Name.equal (snd na) (snd na') || Name.is_anonymous (snd na')
+ if Name.equal (na.CAst.v) (na'.CAst.v) || Name.is_anonymous (na'.CAst.v)
then
let assum = CLocalAssum([na],bk,nal't) in
let new_rest = if nal' = [] then rest else (CLocalAssum(nal',bk',nal't)::rest) in
@@ -638,7 +638,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
let _is_struct =
match fixpoint_exprl with
| [((_,(wf_x,Constrexpr.CWfRec wf_rel),_,_,_),_) as fixpoint_expr] ->
- let (((((_,name),pl),_,args,types,body)),_) as fixpoint_expr =
+ let (((({CAst.v=name},pl),_,args,types,body)),_) as fixpoint_expr =
match recompute_binder_list [fixpoint_expr] with
| [e] -> e
| _ -> assert false
@@ -659,10 +659,10 @@ let do_generate_principle pconstants on_error register_built interactive_proof
true
in
if register_built
- then register_wf name rec_impls wf_rel (map_option snd wf_x) using_lemmas args types body pre_hook;
+ then register_wf name rec_impls wf_rel (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook;
false
|[((_,(wf_x,Constrexpr.CMeasureRec(wf_mes,wf_rel_opt)),_,_,_),_) as fixpoint_expr] ->
- let (((((_,name),_),_,args,types,body)),_) as fixpoint_expr =
+ let (((({CAst.v=name},_),_,args,types,body)),_) as fixpoint_expr =
match recompute_binder_list [fixpoint_expr] with
| [e] -> e
| _ -> assert false
@@ -683,7 +683,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
true
in
if register_built
- then register_mes name rec_impls wf_mes wf_rel_opt (map_option snd wf_x) using_lemmas args types body pre_hook;
+ then register_mes name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook;
true
| _ ->
List.iter (function ((_na,(_,ord),_args,_body,_type),_not) ->
@@ -696,7 +696,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
fixpoint_exprl;
let fixpoint_exprl = recompute_binder_list fixpoint_exprl in
let fix_names =
- List.map (function ((((_,name),_),_,_,_,_),_) -> name) fixpoint_exprl
+ List.map (function ((({CAst.v=name},_),_,_,_,_),_) -> name) fixpoint_exprl
in
(* ok all the expressions are structural *)
let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
@@ -757,7 +757,7 @@ let rec add_args id new_args = CAst.map (function
List.map (fun (b,na,b_option) ->
add_args id new_args b,
na, b_option) cel,
- List.map (fun (loc,(cpl,e)) -> Loc.tag ?loc @@ (cpl,add_args id new_args e)) cal
+ List.map CAst.(map (fun (cpl,e) -> (cpl,add_args id new_args e))) cal
)
| CLetTuple(nal,(na,b_option),b1,b2) ->
CLetTuple(nal,(na,Option.map (add_args id new_args) b_option),
@@ -875,7 +875,7 @@ let make_graph (f_ref:global_reference) =
let l =
List.map
(fun (id,(n,recexp),bl,t,b) ->
- let loc, rec_id = Option.get n in
+ let { CAst.loc; v=rec_id } = Option.get n in
let new_args =
List.flatten
(List.map
@@ -883,7 +883,7 @@ let make_graph (f_ref:global_reference) =
| Constrexpr.CLocalDef (na,_,_)-> []
| Constrexpr.CLocalAssum (nal,_,_) ->
List.map
- (fun (loc,n) -> CAst.make ?loc @@
+ (fun {CAst.loc;v=n} -> CAst.make ?loc @@
CRef(Libnames.Ident(loc, Nameops.Name.get_id n),None))
nal
| Constrexpr.CLocalPattern _ -> assert false
@@ -891,21 +891,21 @@ let make_graph (f_ref:global_reference) =
nal_tas
)
in
- let b' = add_args (snd id) new_args b in
- ((((id,None), ( Some (Loc.tag rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
+ let b' = add_args id.CAst.v new_args b in
+ ((((id,None), ( Some CAst.(make rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
)
fixexprl
in
l
| _ ->
let id = Label.to_id (Constant.label c) in
- [(((Loc.tag id),None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
+ [((CAst.make id,None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
in
let mp,dp,_ = Constant.repr3 c in
do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list;
(* We register the infos *)
List.iter
- (fun ((((_,id),_),_,_,_,_),_) -> add_Function false (Constant.make3 mp dp (Label.of_id id)))
+ (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make3 mp dp (Label.of_id id)))
expr_list)
let do_generate_principle = do_generate_principle [] warning_error true
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 7d2c4d082..794a28dd4 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -346,7 +346,7 @@ let () = register_list_tactical "solve" Tacticals.New.tclSOLVE
let initial_tacticals () =
let idn n = Id.of_string (Printf.sprintf "_%i" n) in
- let varn n = Reference (ArgVar (None, idn n)) in
+ let varn n = Reference (ArgVar (CAst.make (idn n))) in
let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in
List.iter iter [
"first", TacFun ([Name (idn 0)], TacML (None, (initial_entry "first", [varn 0])));
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 4c6d3c2d3..2eb1ef315 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -81,7 +81,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
@@ -102,7 +102,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 =
@@ -188,7 +188,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
@@ -199,7 +199,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 () () ()
@@ -228,11 +228,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
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index 00668ddc7..000c3d2fb 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -50,7 +50,7 @@ val lglob : constr_expr Pcoq.Gram.entry
type 'id gen_place= ('id * Locus.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
val wit_hloc : (loc_place, loc_place, place) Genarg.genarg_type
@@ -77,6 +77,6 @@ val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry
val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type
val wit_in_clause :
- (Id.t Loc.located Locus.clause_expr,
- Id.t Loc.located Locus.clause_expr,
- Id.t Locus.clause_expr) Genarg.genarg_type
+ (lident Locus.clause_expr,
+ lident Locus.clause_expr,
+ Id.t Locus.clause_expr) Genarg.genarg_type
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 286f9d95d..10be8a842 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -71,7 +71,7 @@ END
let induction_arg_of_quantified_hyp = function
| AnonHyp n -> None,ElimOnAnonHyp n
- | NamedHyp id -> None,ElimOnIdent (Loc.tag id)
+ | NamedHyp id -> None,ElimOnIdent (CAst.make 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
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 9ef819569..85c9fc5fd 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -37,10 +37,10 @@ let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c
let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac
let reference_to_id = function
- | Libnames.Ident (loc, id) -> (loc, id)
+ | Libnames.Ident (loc, id) -> CAst.make ?loc id
| Libnames.Qualid (loc,_) ->
- CErrors.user_err ?loc
- (str "This expression should be a simple identifier.")
+ CErrors.user_err ?loc
+ (str "This expression should be a simple identifier.")
let tactic_mode = Gram.entry_create "vernac:tactic_command"
@@ -196,7 +196,7 @@ GEXTEND Gram
verbose most of the time. *)
fresh_id:
[ [ s = STRING -> ArgArg s (*| id = ident -> ArgVar (!@loc,id)*)
- | qid = qualid -> let (_pth,id) = Libnames.repr_qualid (snd qid) in ArgVar (Loc.tag ~loc:!@loc id) ] ]
+ | qid = qualid -> let (_pth,id) = Libnames.repr_qualid (snd qid) in ArgVar (CAst.make ~loc:!@loc id) ] ]
;
constr_eval:
[ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
@@ -225,12 +225,12 @@ GEXTEND Gram
| l = ident -> Name.Name l ] ]
;
let_clause:
- [ [ (l,id) = identref; ":="; te = tactic_expr ->
- ((l,Name id), arg_of_expr te)
- | na = ["_" -> (Some !@loc,Anonymous)]; ":="; te = tactic_expr ->
+ [ [ idr = identref; ":="; te = tactic_expr ->
+ (CAst.map (fun id -> Name id) idr, arg_of_expr te)
+ | na = ["_" -> CAst.make ~loc:!@loc Anonymous]; ":="; te = tactic_expr ->
(na, arg_of_expr te)
- | (l,id) = identref; args = LIST1 input_fun; ":="; te = tactic_expr ->
- ((l,Name id), arg_of_expr (TacFun(args,te))) ] ]
+ | idr = identref; args = LIST1 input_fun; ":="; te = tactic_expr ->
+ (CAst.map (fun id -> Name id) idr, arg_of_expr (TacFun(args,te))) ] ]
;
match_pattern:
[ [ IDENT "context"; oid = OPT Constr.ident;
@@ -483,7 +483,7 @@ let pr_ltac_ref = Libnames.pr_reference
let pr_tacdef_body tacdef_body =
let id, redef, body =
match tacdef_body with
- | TacticDefinition ((_,id), body) -> Id.print id, false, body
+ | TacticDefinition ({CAst.v=id}, body) -> Id.print id, false, body
| TacticRedefinition (id, body) -> pr_ltac_ref id, true, body
in
let idl, body =
@@ -504,7 +504,7 @@ END
VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition
| [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [
VtSideff (List.map (function
- | TacticDefinition ((_,r),_) -> r
+ | TacticDefinition ({CAst.v=r},_) -> r
| TacticRedefinition (Ident (_,r),_) -> r
| TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater
] -> [ fun ~atts ~st -> let open Vernacinterp in
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index e68140828..338d61e6f 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -115,16 +115,16 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
match bl,ann with
[([_],_,_)], None -> 1
| _, Some x ->
- let ids = List.map snd (List.flatten (List.map (fun (nal,_,_) -> nal) bl)) in
- (try List.index Names.Name.equal (snd x) ids
+ let ids = List.map (fun x -> x.CAst.v) (List.flatten (List.map (fun (nal,_,_) -> nal) bl)) in
+ (try List.index Names.Name.equal x.CAst.v ids
with Not_found -> user_err Pp.(str "No such fix variable."))
| _ -> user_err Pp.(str "Cannot guess decreasing argument of fix.") in
let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in
(id,n, CAst.make ~loc @@ CProdN(bl,ty))
let mk_cofix_tac (loc,id,bl,ann,ty) =
- let _ = Option.map (fun (aloc,_) ->
- user_err ~loc:aloc
+ let _ = Option.map (fun { CAst.loc = aloc } ->
+ user_err ?loc:aloc
~hdr:"Constr:mk_cofix_tac"
(Pp.str"Annotation forbidden in cofix expression.")) ann in
let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in
@@ -134,7 +134,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) =
let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
| NoBindings ->
begin
- try ElimOnIdent (Constrexpr_ops.constr_loc c,snd(Constrexpr_ops.coerce_to_id c))
+ try ElimOnIdent (CAst.make ?loc:(Constrexpr_ops.constr_loc c) (Constrexpr_ops.coerce_to_id c).CAst.v)
with e when CErrors.noncritical e -> ElimOnConstr clbind
end
| _ -> ElimOnConstr clbind
@@ -152,6 +152,7 @@ let mkTacCase with_evar = function
(* Reinterpret ident as notations for variables in the context *)
(* because we don't know if they are quantified or not *)
| [(clear,ElimOnIdent id),(None,None),None],None ->
+ let id = CAst.(id.loc, id.v) in
TacCase (with_evar,(clear,(CAst.make @@ CRef (Ident id,None),NoBindings)))
| ic ->
if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic)
@@ -161,7 +162,7 @@ let mkTacCase with_evar = function
let rec mkCLambdaN_simple_loc ?loc bll c =
match bll with
- | ((loc1,_)::_ as idl,bk,t) :: bll ->
+ | ({CAst.loc = loc1}::_ as idl,bk,t) :: bll ->
CAst.make ?loc @@ CLambdaN ([CLocalAssum (idl,bk,t)],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c)
| ([],_,_) :: bll -> mkCLambdaN_simple_loc ?loc bll c
| [] -> c
@@ -169,7 +170,7 @@ let rec mkCLambdaN_simple_loc ?loc bll c =
let mkCLambdaN_simple bl c = match bl with
| [] -> c
| h :: _ ->
- let loc = Loc.merge_opt (fst (List.hd (pi1 h))) (Constrexpr_ops.constr_loc c) in
+ let loc = Loc.merge_opt (List.hd (pi1 h)).CAst.loc (Constrexpr_ops.constr_loc c) in
mkCLambdaN_simple_loc ?loc bl c
let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l))
@@ -381,15 +382,20 @@ GEXTEND Gram
;
hypident:
[ [ id = id_or_meta ->
- id,InHyp
+ let id : Misctypes.lident = id in
+ id,InHyp
| "("; IDENT "type"; IDENT "of"; id = id_or_meta; ")" ->
- id,InHypTypeOnly
+ let id : Misctypes.lident = id in
+ id,InHypTypeOnly
| "("; IDENT "value"; IDENT "of"; id = id_or_meta; ")" ->
- id,InHypValueOnly
+ let id : Misctypes.lident = id in
+ id,InHypValueOnly
] ]
;
hypident_occ:
- [ [ (id,l)=hypident; occs=occs -> ((occs,id),l) ] ]
+ [ [ (id,l)=hypident; occs=occs ->
+ let id : Misctypes.lident = id in
+ ((occs,id),l) ] ]
;
in_clause:
[ [ "*"; occs=occs ->
@@ -433,7 +439,8 @@ GEXTEND Gram
| -> true ]]
;
simple_binder:
- [ [ na=name -> ([na],Default Explicit, CAst.make ~loc:!@loc @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None))
+ [ [ na=name -> ([na],Default Explicit, CAst.make ~loc:!@loc @@
+ CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None))
| "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c)
] ]
;
@@ -565,28 +572,34 @@ GEXTEND Gram
TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,c,p,false,e))
(* Alternative syntax for "pose proof c as id" *)
- | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
+ | IDENT "assert"; test_lpar_id_coloneq; "("; lid = identref; ":=";
c = lconstr; ")" ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,None,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
- | IDENT "eassert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
+ let { CAst.loc = loc; v = id } = lid in
+ TacAtom (Loc.tag ?loc @@ TacAssert (false,true,None,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c))
+ | IDENT "eassert"; test_lpar_id_coloneq; "("; lid = identref; ":=";
c = lconstr; ")" ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,None,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
+ let { CAst.loc = loc; v = id } = lid in
+ TacAtom (Loc.tag ?loc @@ TacAssert (true,true,None,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c))
(* Alternative syntax for "assert c as id by tac" *)
- | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
+ | IDENT "assert"; test_lpar_id_colon; "("; lid = identref; ":";
c = lconstr; ")"; tac=by_tactic ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
- | IDENT "eassert"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
+ let { CAst.loc = loc; v = id } = lid in
+ TacAtom (Loc.tag ?loc @@ TacAssert (false,true,Some tac,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c))
+ | IDENT "eassert"; test_lpar_id_colon; "("; lid = identref; ":";
c = lconstr; ")"; tac=by_tactic ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
+ let { CAst.loc = loc; v = id } = lid in
+ TacAtom (Loc.tag ?loc @@ TacAssert (true,true,Some tac,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c))
(* Alternative syntax for "enough c as id by tac" *)
- | IDENT "enough"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
+ | IDENT "enough"; test_lpar_id_colon; "("; lid = identref; ":";
c = lconstr; ")"; tac=by_tactic ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,false,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
- | IDENT "eenough"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
+ let { CAst.loc = loc; v = id } = lid in
+ TacAtom (Loc.tag ?loc @@ TacAssert (false,false,Some tac,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c))
+ | IDENT "eenough"; test_lpar_id_colon; "("; lid = identref; ":";
c = lconstr; ")"; tac=by_tactic ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,false,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
+ let { CAst.loc = loc; v = id } = lid in
+ TacAtom (Loc.tag ?loc @@ TacAssert (true,false,Some tac,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c))
| IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic ->
TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,ipat,c))
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 048dcc8e9..ecb0b5796 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -9,7 +9,6 @@
(** Ltac parsing entries *)
open Loc
-open Names
open Pcoq
open Libnames
open Constrexpr
@@ -20,7 +19,7 @@ open Misctypes
val open_constr : constr_expr Gram.entry
val constr_with_bindings : constr_expr with_bindings Gram.entry
val bindings : constr_expr bindings Gram.entry
-val hypident : (Id.t located * Locus.hyp_location_flag) Gram.entry
+val hypident : (lident * Locus.hyp_location_flag) Gram.entry
val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
val uconstr : constr_expr Gram.entry
@@ -29,8 +28,8 @@ val destruction_arg : constr_expr with_bindings destruction_arg Gram.entry
val int_or_var : int or_var Gram.entry
val simple_tactic : raw_tactic_expr Gram.entry
val simple_intropattern : constr_expr intro_pattern_expr located Gram.entry
-val in_clause : Names.Id.t Loc.located Locus.clause_expr Gram.entry
-val clause_dft_concl : Names.Id.t Loc.located Locus.clause_expr Gram.entry
+val in_clause : lident Locus.clause_expr Gram.entry
+val clause_dft_concl : lident Locus.clause_expr Gram.entry
val tactic_arg : raw_tactic_arg Gram.entry
val tactic_expr : raw_tactic_expr Gram.entry
val binder_tactic : raw_tactic_expr Gram.entry
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 4f430b79e..3bc9f2aa0 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -161,7 +161,7 @@ let string_of_genarg_arg (ArgumentType arg) =
(keyword "eval" ++ brk (1,1) ++
pr_red_expr (prc,prlc,pr2,pr3) r ++ spc () ++
keyword "in" ++ spc() ++ prc c)
- | ConstrContext ((_,id),c) ->
+ | ConstrContext ({CAst.v=id},c) ->
hov 0
(keyword "context" ++ spc () ++ pr_id id ++ spc () ++
str "[ " ++ prlc c ++ str " ]")
@@ -364,7 +364,7 @@ let string_of_genarg_arg (ArgumentType arg) =
let pr_ltac_or_var pr = function
| ArgArg x -> pr x
- | ArgVar (loc,id) -> pr_with_comments ?loc (pr_id id)
+ | ArgVar {CAst.loc;v=id} -> pr_with_comments ?loc (pr_id id)
let pr_ltac_constant kn =
if !Flags.in_debugger then KerName.print kn
@@ -404,7 +404,7 @@ let string_of_genarg_arg (ArgumentType arg) =
let pr_as_name = function
| Anonymous -> mt ()
- | Name id -> spc () ++ keyword "as" ++ spc () ++ pr_lident (Loc.tag id)
+ | Name id -> spc () ++ keyword "as" ++ spc () ++ pr_lident (CAst.make id)
let pr_pose_as_style prc na c =
spc() ++ prc c ++ pr_as_name na
@@ -496,12 +496,12 @@ let string_of_genarg_arg (ArgumentType arg) =
let pr_core_destruction_arg prc prlc = function
| ElimOnConstr c -> pr_with_bindings prc prlc c
- | ElimOnIdent (loc,id) -> pr_with_comments ?loc (pr_id id)
+ | ElimOnIdent {CAst.loc;v=id} -> pr_with_comments ?loc (pr_id id)
| ElimOnAnonHyp n -> int n
let pr_destruction_arg prc prlc (clear_flag,h) =
pr_clear_flag clear_flag (pr_core_destruction_arg prc prlc) h
-
+
let pr_inversion_kind = function
| SimpleInversion -> primitive "simple inversion"
| FullInversion -> primitive "inversion"
@@ -684,7 +684,7 @@ let pr_goal_selector ~toplevel s =
(* match t with
| CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal
| _ ->*)
- let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in
+ let s = prlist_with_sep spc Ppconstr.pr_lname nal ++ str ":" ++ pr.pr_lconstr t in
spc() ++ hov 1 (str"(" ++ s ++ str")") in
let pr_fix_tac (id,n,c) =
@@ -692,10 +692,10 @@ let pr_goal_selector ~toplevel s =
(nal,ty)::bll ->
if n <= List.length nal then
match List.chop (n-1) nal with
- _, (_,Name id) :: _ -> id, (nal,ty)::bll
- | bef, (loc,Anonymous) :: aft ->
+ _, {CAst.v=Name id} :: _ -> id, (nal,ty)::bll
+ | bef, {CAst.loc;v=Anonymous} :: aft ->
let id = next_ident_away (Id.of_string"y") avoid in
- id, ((bef@(loc,Name id)::aft, ty)::bll)
+ id, ((bef@(CAst.make ?loc @@ Name id)::aft, ty)::bll)
| _ -> assert false
else
let (id,bll') = set_nth_name avoid (n-List.length nal) bll in
@@ -705,7 +705,7 @@ let pr_goal_selector ~toplevel s =
let names =
List.fold_left
(fun ln (nal,_) -> List.fold_left
- (fun ln na -> match na with (_,Name id) -> Id.Set.add id ln | _ -> ln)
+ (fun ln na -> match na with { CAst.v=Name id } -> Id.Set.add id ln | _ -> ln)
ln nal)
Id.Set.empty bll in
let idarg,bll = set_nth_name names n bll in
@@ -1087,7 +1087,7 @@ let pr_goal_selector ~toplevel s =
if Int.equal n 0 then (List.rev acc, (ty,None)) else
match DAst.get ty with
Glob_term.GProd(na,Explicit,a,b) ->
- strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b
+ strip_ty (([CAst.make na],(a,None))::acc) (n-1) b
| _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
strip_ty [] n ty
@@ -1158,7 +1158,7 @@ let pr_goal_selector ~toplevel s =
if n=0 then (List.rev acc, EConstr.of_constr ty) else
match Constr.kind ty with
| Constr.Prod(na,a,b) ->
- strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b
+ strip_ty (([CAst.make na],EConstr.of_constr a)::acc) (n-1) b
| _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
strip_ty [] n ty
@@ -1318,7 +1318,7 @@ let () =
register_basic_print0 wit_ref
pr_reference (pr_or_var (pr_located pr_global)) pr_global;
register_basic_print0 wit_ident pr_id pr_id pr_id;
- register_basic_print0 wit_var (pr_located pr_id) (pr_located pr_id) pr_id;
+ register_basic_print0 wit_var pr_lident pr_lident pr_id;
register_print0
wit_intro_pattern
(lift (Miscprint.pr_intro_pattern pr_constr_expr))
@@ -1328,7 +1328,7 @@ let () =
wit_clause_dft_concl
(lift (pr_clauses (Some true) pr_lident))
(lift (pr_clauses (Some true) pr_lident))
- (fun c -> Genprint.TopPrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)) c))
+ (fun c -> Genprint.TopPrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (CAst.make id)) c))
;
Genprint.register_print0
wit_constr
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index acd7a30c4..e73a18b79 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1773,7 +1773,7 @@ let rec strategy_of_ast = function
let mkappc s l = CAst.make @@ CAppExpl ((None,(Libnames.Ident (Loc.tag @@ Id.of_string s)),None),l)
let declare_an_instance n s args =
- (((Loc.tag @@ Name n),None), Explicit,
+ (((CAst.make @@ Name n),None), Explicit,
CAst.make @@ CAppExpl ((None, Qualid (Loc.tag @@ qualid_of_string s),None),
args))
@@ -2006,7 +2006,7 @@ let add_morphism glob binders m s n =
let poly = Flags.is_universe_polymorphism () in
let instance_id = add_suffix n "_Proper" in
let instance =
- (((Loc.tag @@ Name instance_id),None), Explicit,
+ (((CAst.make @@ Name instance_id),None), Explicit,
CAst.make @@ CAppExpl (
(None, Qualid (Loc.tag @@ Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None),
[cHole; s; m]))
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 8112cc400..4313456a4 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -374,7 +374,7 @@ let add_ml_tactic_notation name ~level prods =
in
let ids = List.map_filter get_id prods in
let entry = { mltac_name = name; mltac_index = len - i - 1 } in
- let map id = Reference (Misctypes.ArgVar (Loc.tag id)) in
+ let map id = Reference (Misctypes.ArgVar (CAst.make id)) in
let tac = TacML (Loc.tag (entry, List.map map ids)) in
add_glob_tactic_notation false ~level prods true ids tac
in
@@ -431,11 +431,11 @@ let warn_unusable_identifier =
let register_ltac local tacl =
let map tactic_body =
match tactic_body with
- | Tacexpr.TacticDefinition ((loc,id), body) ->
+ | Tacexpr.TacticDefinition ({CAst.loc;v=id}, body) ->
let kn = Lib.make_kn id in
let id_pp = Id.print id in
let () = if is_defined_tac kn then
- CErrors.user_err ?loc
+ CErrors.user_err ?loc
(str "There is already an Ltac named " ++ id_pp ++ str".")
in
let is_shadowed =
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index ccd555b61..146d8300d 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -41,7 +41,7 @@ type goal_selector = Vernacexpr.goal_selector =
type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg =
| ElimOnConstr of 'a
- | ElimOnIdent of Id.t located
+ | ElimOnIdent of lident
| ElimOnAnonHyp of int
type 'a destruction_arg =
@@ -85,8 +85,8 @@ type 'a match_pattern =
(* Type of hypotheses for a Match Context rule *)
type 'a match_context_hyps =
- | Hyp of Name.t located * 'a match_pattern
- | Def of Name.t located * 'a match_pattern * 'a match_pattern
+ | Hyp of lname * 'a match_pattern
+ | Def of lname * 'a match_pattern * 'a match_pattern
(* Type of a Match rule for Match Context and Match *)
type ('a,'t) match_rule =
@@ -254,7 +254,7 @@ and 'a gen_tactic_expr =
| TacFail of global_flag * int or_var * 'n message_token list
| TacInfo of 'a gen_tactic_expr
| TacLetIn of rec_flag *
- (Name.t located * 'a gen_tactic_arg) list *
+ (lname * 'a gen_tactic_arg) list *
'a gen_tactic_expr
| TacMatch of lazy_flag *
'a gen_tactic_expr *
@@ -300,7 +300,7 @@ type g_trm = glob_constr_and_expr
type g_pat = glob_constr_pattern_and_expr
type g_cst = evaluable_global_reference and_short_name or_var
type g_ref = ltac_constant located or_var
-type g_nam = Id.t located
+type g_nam = lident
type g_dispatch = <
term:g_trm;
@@ -328,7 +328,7 @@ type r_trm = constr_expr
type r_pat = constr_pattern_expr
type r_cst = reference or_by_notation
type r_ref = reference
-type r_nam = Id.t located
+type r_nam = lident
type r_lev = rlevel
type r_dispatch = <
@@ -357,7 +357,7 @@ type t_trm = EConstr.constr
type t_pat = constr_pattern
type t_cst = evaluable_global_reference
type t_ref = ltac_constant located
-type t_nam = Id.t
+type t_nam = Id.t
type t_dispatch = <
term:t_trm;
@@ -391,5 +391,5 @@ type ltac_call_kind =
type ltac_trace = ltac_call_kind Loc.located list
type tacdef_body =
- | TacticDefinition of Id.t Loc.located * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *)
+ | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *)
| TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index ebffde441..22ec6c5b1 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -6,12 +6,13 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pattern
open Pp
+open CErrors
+open CAst
+open Pattern
open Genredexpr
open Glob_term
open Tacred
-open CErrors
open Util
open Names
open Libnames
@@ -73,11 +74,11 @@ let strict_check = ref false
let adjust_loc loc = if !strict_check then None else loc
(* Globalize a name which must be bound -- actually just check it is bound *)
-let intern_hyp ist (loc,id as locid) =
+let intern_hyp ist ({loc;v=id} as locid) =
if not !strict_check then
locid
else if find_ident id ist then
- Loc.tag id
+ make id
else
Pretype_errors.error_var_not_found ?loc id
@@ -89,7 +90,8 @@ let intern_int_or_var = intern_or_var (fun (n : int) -> n)
let intern_string_or_var = intern_or_var (fun (s : string) -> s)
let intern_global_reference ist = function
- | Ident (loc,id) when find_var id ist -> ArgVar (loc,id)
+ | Ident (loc,id) when find_var id ist ->
+ ArgVar CAst.(make ?loc id)
| r ->
let loc,_ as lqid = qualid_of_reference r in
try ArgArg (loc,locate_global_with_alias lqid)
@@ -99,7 +101,7 @@ let intern_ltac_variable ist = function
| Ident (loc,id) ->
if find_var id ist then
(* A local variable of any type *)
- ArgVar (loc,id)
+ ArgVar CAst.(make ?loc id)
else raise Not_found
| _ ->
raise Not_found
@@ -249,7 +251,7 @@ and intern_or_and_intro_pattern lf ist = function
IntroOrPattern (List.map (List.map (intern_intro_pattern lf ist)) ll)
let intern_or_and_intro_pattern_loc lf ist = function
- | ArgVar (_,id) as x ->
+ | ArgVar {v=id} as x ->
if find_var id ist then x
else user_err Pp.(str "Disjunctive/conjunctive introduction pattern expected.")
| ArgArg (loc,l) -> ArgArg (loc,intern_or_and_intro_pattern lf ist l)
@@ -261,18 +263,18 @@ let intern_intro_pattern_naming_loc lf ist (loc,pat) =
let intern_destruction_arg ist = function
| clear,ElimOnConstr c -> clear,ElimOnConstr (intern_constr_with_bindings ist c)
| clear,ElimOnAnonHyp n as x -> x
- | clear,ElimOnIdent (loc,id) ->
+ | clear,ElimOnIdent {loc;v=id} ->
if !strict_check then
(* If in a defined tactic, no intros-until *)
let c, p = intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) in
match DAst.get c with
- | GVar id -> clear,ElimOnIdent (c.CAst.loc,id)
+ | GVar id -> clear,ElimOnIdent CAst.(make ?loc:c.loc id)
| _ -> clear,ElimOnConstr ((c, p), NoBindings)
else
- clear,ElimOnIdent (loc,id)
+ clear,ElimOnIdent CAst.(make ?loc id)
let short_name = function
- | AN (Ident (loc,id)) when not !strict_check -> Some (loc,id)
+ | AN (Ident (loc,id)) when not !strict_check -> Some CAst.(make ?loc id)
| _ -> None
let intern_evaluable_global_reference ist r =
@@ -292,9 +294,9 @@ let intern_evaluable_reference_or_by_notation ist = function
(* Globalize a reduction expression *)
let intern_evaluable ist = function
- | AN (Ident (loc,id)) when find_var id ist -> ArgVar (loc,id)
+ | AN (Ident (loc,id)) when find_var id ist -> ArgVar CAst.(make ?loc id)
| AN (Ident (loc,id)) when not !strict_check && find_hyp id ist ->
- ArgArg (EvalVarRef id, Some (loc,id))
+ ArgArg (EvalVarRef id, Some CAst.(make ?loc id))
| r ->
let e = intern_evaluable_reference_or_by_notation ist r in
let na = short_name r in
@@ -370,7 +372,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
Inr (bound_names,(c,None),dummy_pat) in
(l, match p with
| Inl r -> interp_ref r
- | Inr { CAst.v = CAppExpl((None,r,None),[]) } ->
+ | Inr { v = CAppExpl((None,r,None),[]) } ->
(* We interpret similarly @ref and ref *)
interp_ref (AN r)
| Inr c ->
@@ -400,8 +402,8 @@ let intern_red_expr ist = function
| Lazy f -> Lazy (intern_flag ist f)
| Pattern l -> Pattern (List.map (intern_constr_with_occurrences ist) l)
| Simpl (f,o) ->
- Simpl (intern_flag ist f,
- Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
+ Simpl (intern_flag ist f,
+ Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
| CbvVm o -> CbvVm (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
| CbvNative o -> CbvNative (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
| (Red _ | Hnf | ExtraRedExpr _ as r ) -> r
@@ -438,7 +440,7 @@ let intern_pattern ist ?(as_type=false) ltacvars = function
let intern_constr_may_eval ist = function
| ConstrEval (r,c) -> ConstrEval (intern_red_expr ist r,intern_constr ist c)
| ConstrContext (locid,c) ->
- ConstrContext (intern_hyp ist locid,intern_constr ist c)
+ ConstrContext (intern_hyp ist locid,intern_constr ist c)
| ConstrTypeOf c -> ConstrTypeOf (intern_constr ist c)
| ConstrTerm c -> ConstrTerm (intern_constr ist c)
@@ -452,12 +454,12 @@ let opt_cons accu = function
(* Reads the hypotheses of a "match goal" rule *)
let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function
- | (Hyp ((_,na) as locna,mp))::tl ->
+ | (Hyp ({v=na} as locna,mp))::tl ->
let ido, metas1, pat = intern_pattern ist ~as_type:true lfun mp in
let lfun, metas2, hyps = intern_match_goal_hyps ist lfun tl in
let lfun' = name_cons (opt_cons lfun ido) na in
lfun', metas1@metas2, Hyp (locna,pat)::hyps
- | (Def ((_,na) as locna,mv,mp))::tl ->
+ | (Def ({v=na} as locna,mv,mp))::tl ->
let ido, metas1, patv = intern_pattern ist ~as_type:false lfun mv in
let ido', metas2, patt = intern_pattern ist ~as_type:true lfun mp in
let lfun, metas3, hyps = intern_match_goal_hyps ist ~as_type lfun tl in
@@ -467,7 +469,7 @@ let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function
(* Utilities *)
let extract_let_names lrc =
- let fold accu ((loc, name), _) =
+ let fold accu ({loc;v=name}, _) =
Nameops.Name.fold_right (fun id accu ->
if Id.Set.mem id accu then user_err ?loc
~hdr:"glob_tactic" (str "This variable is bound several times.")
@@ -813,7 +815,7 @@ let notation_subst bindings tac =
let fold id c accu =
let loc = Glob_ops.loc_of_glob_constr (fst c) in
let c = ConstrMayEval (ConstrTerm c) in
- ((loc, Name id), c) :: accu
+ (CAst.make ?loc @@ Name id, c) :: accu
in
let bindings = Id.Map.fold fold bindings [] in
(** This is theoretically not correct due to potential variable capture, but
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index e3a4d5c79..8021dc715 100644
--- a/plugins/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
@@ -47,7 +47,7 @@ val intern_constr_with_bindings :
glob_sign -> constr_expr * constr_expr bindings ->
glob_constr_and_expr * glob_constr_and_expr bindings
-val intern_hyp : glob_sign -> Id.t Loc.located -> Id.t Loc.located
+val intern_hyp : glob_sign -> lident -> lident
(** Adds a globalization function for extra generic arguments *)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index f2720954d..79b5c1622 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -9,6 +9,7 @@
open Constrintern
open Patternops
open Pp
+open CAst
open Genredexpr
open Glob_term
open Glob_ops
@@ -363,16 +364,16 @@ let error_ltac_variable ?loc id env v s =
strbrk "which cannot be coerced to " ++ str s ++ str".")
(* Raise Not_found if not in interpretation sign *)
-let try_interp_ltac_var coerce ist env (loc,id) =
+let try_interp_ltac_var coerce ist env {loc;v=id} =
let v = Id.Map.find id ist.lfun in
try coerce v with CannotCoerceTo s -> error_ltac_variable ?loc id env v s
let interp_ltac_var coerce ist env locid =
try try_interp_ltac_var coerce ist env locid
- with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time.")
+ with Not_found -> anomaly (str "Detected '" ++ Id.print locid.v ++ str "' as ltac var at interning time.")
let interp_ident ist env sigma id =
- try try_interp_ltac_var (coerce_var_to_ident false env sigma) ist (Some (env,sigma)) (Loc.tag id)
+ try try_interp_ltac_var (coerce_var_to_ident false env sigma) ist (Some (env,sigma)) (make id)
with Not_found -> id
(* Interprets an optional identifier, bound or fresh *)
@@ -381,25 +382,25 @@ let interp_name ist env sigma = function
| Name id -> Name (interp_ident ist env sigma id)
let interp_intro_pattern_var loc ist env sigma id =
- try try_interp_ltac_var (coerce_to_intro_pattern env sigma) ist (Some (env,sigma)) (loc,id)
+ try try_interp_ltac_var (coerce_to_intro_pattern env sigma) ist (Some (env,sigma)) (make ?loc id)
with Not_found -> IntroNaming (IntroIdentifier id)
let interp_intro_pattern_naming_var loc ist env sigma id =
- try try_interp_ltac_var (coerce_to_intro_pattern_naming env sigma) ist (Some (env,sigma)) (loc,id)
+ try try_interp_ltac_var (coerce_to_intro_pattern_naming env sigma) ist (Some (env,sigma)) (make ?loc id)
with Not_found -> IntroIdentifier id
-let interp_int ist locid =
+let interp_int ist ({loc;v=id} as locid) =
try try_interp_ltac_var coerce_to_int ist None locid
with Not_found ->
- user_err ?loc:(fst locid) ~hdr:"interp_int"
- (str "Unbound variable " ++ Id.print (snd locid) ++ str".")
+ user_err ?loc ~hdr:"interp_int"
+ (str "Unbound variable " ++ Id.print id ++ str".")
let interp_int_or_var ist = function
| ArgVar locid -> interp_int ist locid
| ArgArg n -> n
let interp_int_or_var_as_list ist = function
- | ArgVar (_,id as locid) ->
+ | ArgVar ({v=id} as locid) ->
(try coerce_to_int_or_var_list (Id.Map.find id ist.lfun)
with Not_found | CannotCoerceTo _ -> [ArgArg (interp_int ist locid)])
| ArgArg n as x -> [x]
@@ -408,7 +409,7 @@ let interp_int_or_var_list ist l =
List.flatten (List.map (interp_int_or_var_as_list ist) l)
(* Interprets a bound variable (especially an existing hypothesis) *)
-let interp_hyp ist env sigma (loc,id as locid) =
+let interp_hyp ist env sigma ({loc;v=id} as locid) =
(* Look first in lfun for a value coercible to a variable *)
try try_interp_ltac_var (coerce_to_hyp env sigma) ist (Some (env,sigma)) locid
with Not_found ->
@@ -416,7 +417,7 @@ let interp_hyp ist env sigma (loc,id as locid) =
if is_variable env id then id
else Loc.raise ?loc (Logic.RefinerError (env, sigma, Logic.NoSuchHyp id))
-let interp_hyp_list_as_list ist env sigma (loc,id as x) =
+let interp_hyp_list_as_list ist env sigma ({loc;v=id} as x) =
try coerce_to_hyp_list env sigma (Id.Map.find id ist.lfun)
with Not_found | CannotCoerceTo _ -> [interp_hyp ist env sigma x]
@@ -425,8 +426,8 @@ let interp_hyp_list ist env sigma l =
let interp_reference ist env sigma = function
| ArgArg (_,r) -> r
- | ArgVar (loc, id) ->
- try try_interp_ltac_var (coerce_to_reference env sigma) ist (Some (env,sigma)) (loc, id)
+ | ArgVar {loc;v=id} ->
+ try try_interp_ltac_var (coerce_to_reference env sigma) ist (Some (env,sigma)) (make ?loc id)
with Not_found ->
try
VarRef (get_id (Environ.lookup_named id env))
@@ -439,7 +440,7 @@ let try_interp_evaluable env (loc, id) =
| _ -> error_not_evaluable (VarRef id)
let interp_evaluable ist env sigma = function
- | ArgArg (r,Some (loc,id)) ->
+ | ArgArg (r,Some {loc;v=id}) ->
(* Maybe [id] has been introduced by Intro-like tactics *)
begin
try try_interp_evaluable env (loc, id)
@@ -449,8 +450,8 @@ let interp_evaluable ist env sigma = function
| _ -> error_global_not_found ?loc (qualid_of_ident id)
end
| ArgArg (r,None) -> r
- | ArgVar (loc, id) ->
- try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (loc, id)
+ | ArgVar {loc;v=id} ->
+ try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id)
with Not_found ->
try try_interp_evaluable env (loc, id)
with Not_found -> error_global_not_found ?loc (qualid_of_ident id)
@@ -521,9 +522,9 @@ let default_fresh_id = Id.of_string "H"
let interp_fresh_id ist env sigma l =
let extract_ident ist env sigma id =
try try_interp_ltac_var (coerce_to_ident_not_fresh env sigma)
- ist (Some (env,sigma)) (Loc.tag id)
+ ist (Some (env,sigma)) (make id)
with Not_found -> id in
- let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in
+ let ids = List.map_filter (function ArgVar {v=id} -> Some id | _ -> None) l in
let avoid = match TacStore.get ist.extra f_avoid_ids with
| None -> Id.Set.empty
| Some l -> l
@@ -535,7 +536,7 @@ let interp_fresh_id ist env sigma l =
let s =
String.concat "" (List.map (function
| ArgArg s -> s
- | ArgVar (_,id) -> Id.to_string (extract_ident ist env sigma id)) l) in
+ | ArgVar {v=id} -> Id.to_string (extract_ident ist env sigma id)) l) in
let s = if CLexer.is_keyword s then s^"0" else s in
Id.of_string s in
Tactics.fresh_id_in_env avoid id env
@@ -701,7 +702,7 @@ let interp_constr_with_occurrences ist env sigma (occs,c) =
let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
let p = match a with
- | Inl (ArgVar (loc,id)) ->
+ | Inl (ArgVar {loc;v=id}) ->
(* This is the encoding of an ltac var supposed to be bound
prioritary to an evaluable reference and otherwise to a constr
(it is an encoding to satisfy the "union" type given to Simpl) *)
@@ -710,7 +711,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
with CannotCoerceTo _ ->
let c = coerce_to_closed_constr env x in
Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in
- (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (loc,id)
+ (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id)
with Not_found ->
error_global_not_found ?loc (qualid_of_ident id))
| Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b)
@@ -756,7 +757,7 @@ let interp_may_eval f ist env sigma = function
let (sigma,c_interp) = f ist env sigma c in
let (redfun, _) = Redexpr.reduction_of_red_expr env redexp in
redfun env sigma c_interp
- | ConstrContext ((loc,s),c) ->
+ | ConstrContext ({loc;v=s},c) ->
(try
let (sigma,ic) = f ist env sigma c in
let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in
@@ -821,7 +822,7 @@ let message_of_value v =
let interp_message_token ist = function
| MsgString s -> Ftactic.return (str s)
| MsgInt n -> Ftactic.return (int n)
- | MsgIdent (loc,id) ->
+ | MsgIdent {loc;v=id} ->
let v = try Some (Id.Map.find id ist.lfun) with Not_found -> None in
match v with
| None -> Ftactic.lift (Tacticals.New.tclZEROMSG (Id.print id ++ str" not found."))
@@ -881,7 +882,7 @@ let interp_intro_pattern_naming_option ist env sigma = function
let interp_or_and_intro_pattern_option ist env sigma = function
| None -> sigma, None
- | Some (ArgVar (loc,id)) ->
+ | Some (ArgVar {loc;v=id}) ->
(match interp_intro_pattern_var loc ist env sigma id with
| IntroAction (IntroOrAndPattern l) -> sigma, Some (loc,l)
| _ ->
@@ -906,14 +907,14 @@ let interp_binding_name ist env sigma = function
(* If a name is bound, it has to be a quantified hypothesis *)
(* user has to use other names for variables if these ones clash with *)
(* a name intented to be used as a (non-variable) identifier *)
- try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist (Some (env,sigma)) (Loc.tag id)
+ try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist (Some (env,sigma)) (make id)
with Not_found -> NamedHyp id
let interp_declared_or_quantified_hypothesis ist env sigma = function
| AnonHyp n -> AnonHyp n
| NamedHyp id ->
try try_interp_ltac_var
- (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (Loc.tag id)
+ (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (make id)
with Not_found -> NamedHyp id
let interp_binding ist env sigma (loc,(b,c)) =
@@ -924,7 +925,7 @@ let interp_bindings ist env sigma = function
| NoBindings ->
sigma, NoBindings
| ImplicitBindings l ->
- let sigma, l = interp_open_constr_list ist env sigma l in
+ let sigma, l = interp_open_constr_list ist env sigma l in
sigma, ImplicitBindings l
| ExplicitBindings l ->
let sigma, l = List.fold_left_map (interp_binding ist env) sigma l in
@@ -959,14 +960,14 @@ let interp_destruction_arg ist gl arg =
interp_open_constr_with_bindings ist env sigma c
end
| keep,ElimOnAnonHyp n as x -> x
- | keep,ElimOnIdent (loc,id) ->
+ | keep,ElimOnIdent {loc;v=id} ->
let error () = user_err ?loc
(strbrk "Cannot coerce " ++ Id.print id ++
strbrk " neither to a quantified hypothesis nor to a term.")
in
let try_cast_id id' =
if Tactics.is_quantified_hypothesis id' gl
- then keep,ElimOnIdent (loc,id')
+ then keep,ElimOnIdent CAst.(make ?loc id')
else
(keep, ElimOnConstr begin fun env sigma ->
try (sigma, (constr_of_id env id', NoBindings))
@@ -994,7 +995,7 @@ let interp_destruction_arg ist gl arg =
with Not_found ->
(* We were in non strict (interactive) mode *)
if Tactics.is_quantified_hypothesis id gl then
- keep,ElimOnIdent (loc,id)
+ keep,ElimOnIdent CAst.(make ?loc id)
else
let c = (DAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in
let f env sigma =
@@ -1043,11 +1044,11 @@ let cons_and_check_name id l =
else id::l
let rec read_match_goal_hyps lfun ist env sigma lidh = function
- | (Hyp ((loc,na) as locna,mp))::tl ->
+ | (Hyp ({loc;v=na} as locna,mp))::tl ->
let lidh' = Name.fold_right cons_and_check_name na lidh in
Hyp (locna,read_pattern lfun ist env sigma mp)::
(read_match_goal_hyps lfun ist env sigma lidh' tl)
- | (Def ((loc,na) as locna,mv,mp))::tl ->
+ | (Def ({loc;v=na} as locna,mv,mp))::tl ->
let lidh' = Name.fold_right cons_and_check_name na lidh in
Def (locna,read_pattern lfun ist env sigma mv, read_pattern lfun ist env sigma mp)::
(read_match_goal_hyps lfun ist env sigma lidh' tl)
@@ -1112,7 +1113,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti
in
Tactic_debug.debug_prompt lev tac eval
| _ -> value_interp ist >>= fun v -> return (name_vfun appl v)
-
+
and eval_tactic ist tac : unit Proofview.tactic = match tac with
| TacAtom (loc,t) ->
@@ -1248,7 +1249,7 @@ and force_vrec ist v : Val.t Ftactic.t =
and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
match r with
- | ArgVar (loc,id) ->
+ | ArgVar {loc;v=id} ->
let v =
try Id.Map.find id ist.lfun
with Not_found -> in_gen (topwit wit_var) id
@@ -1416,7 +1417,7 @@ and tactic_of_value ist vle =
and interp_letrec ist llc u =
Proofview.tclUNIT () >>= fun () -> (* delay for the effects of [lref], just in case. *)
let lref = ref ist.lfun in
- let fold accu ((_, na), b) =
+ let fold accu ({v=na}, b) =
let v = of_tacvalue (VRec (lref, TacArg (Loc.tag b))) in
Name.fold_right (fun id -> Id.Map.add id v) na accu
in
@@ -1431,7 +1432,7 @@ and interp_letin ist llc u =
| [] ->
let ist = { ist with lfun } in
val_interp ist u
- | ((_, na), body) :: defs ->
+ | ({v=na}, body) :: defs ->
Ftactic.bind (interp_tacarg ist body) (fun v ->
fold (Name.fold_right (fun id -> Id.Map.add id v) na lfun) defs)
in
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index 5f2723a1e..2d448e832 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -75,7 +75,7 @@ val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map
(** Interprets tactic expressions *)
val interp_hyp : interp_sign -> Environ.env -> Evd.evar_map ->
- Id.t Loc.located -> Id.t
+ lident -> Id.t
val interp_glob_closure : interp_sign -> Environ.env -> Evd.evar_map ->
?kind:Pretyping.typing_constraint -> ?pattern_mode:bool -> glob_constr_and_expr ->
@@ -125,9 +125,9 @@ val hide_interp : bool -> raw_tactic_expr -> unit Proofview.tactic option -> uni
(** Internals that can be useful for syntax extensions. *)
val interp_ltac_var : (value -> 'a) -> interp_sign ->
- (Environ.env * Evd.evar_map) option -> Id.t Loc.located -> 'a
+ (Environ.env * Evd.evar_map) option -> lident -> 'a
-val interp_int : interp_sign -> Id.t Loc.located -> int
+val interp_int : interp_sign -> lident -> int
val interp_int_or_var : interp_sign -> int or_var -> int
diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli
index 2475e41f9..dce6f5558 100644
--- a/plugins/ltac/tactic_debug.mli
+++ b/plugins/ltac/tactic_debug.mli
@@ -74,7 +74,7 @@ val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t
(** Prints a logic failure message for a rule *)
val db_breakpoint : debug_info ->
- Id.t Loc.located message_token list -> unit Proofview.NonLogical.t
+ Misctypes.lident message_token list -> unit Proofview.NonLogical.t
val extract_ltac_trace :
?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.t option Loc.located
diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index e87951dd7..6bf9215e0 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -306,9 +306,9 @@ module PatternMatching (E:StaticEnvironment) = struct
[pat] is [Hyp _] or [Def _]. *)
let hyp_match pat hyps =
match pat with
- | Hyp ((_,hypname),typepat) ->
+ | Hyp ({CAst.v=hypname},typepat) ->
hyp_match_type hypname typepat hyps
- | Def ((_,hypname),bodypat,typepat) ->
+ | Def ({CAst.v=hypname},bodypat,typepat) ->
hyp_match_body_and_type hypname bodypat typepat hyps
(** [hyp_pattern_list_match pats hyps lhs], matches the list of
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 01d3f79c7..5ce30c3d7 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -255,10 +255,10 @@ let tauto_power_flags = {
}
let with_flags flags _ ist =
- let f = (Loc.tag @@ Id.of_string "f") in
- let x = (Loc.tag @@ Id.of_string "x") in
+ let f = CAst.make @@ Id.of_string "f" in
+ let x = CAst.make @@ Id.of_string "x" in
let arg = Val.Dyn (tag_tauto_flags, flags) in
- let ist = { ist with lfun = Id.Map.add (snd x) arg ist.lfun } in
+ let ist = { ist with lfun = Id.Map.add x.CAst.v arg ist.lfun } in
eval_tactic_ist ist (TacArg (Loc.tag @@ TacCall (Loc.tag (ArgVar f, [Reference (ArgVar x)]))))
let register_tauto_tactic tac name0 args =
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index 40897d62f..55dc7f580 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -22,7 +22,7 @@ let x = Id.of_string "x"
let make_cont (k : Val.t) (c : EConstr.t) =
let c = Tacinterp.Value.of_constr c in
- let tac = TacCall (Loc.tag (ArgVar (Loc.tag cont), [Reference (ArgVar (Loc.tag x))])) in
+ let tac = TacCall (Loc.tag (ArgVar CAst.(make cont), [Reference (ArgVar CAst.(make x))])) in
let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in
Tacinterp.eval_tactic_ist ist (TacArg (Loc.tag tac))
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index e3e749b75..125afb1a0 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -166,12 +166,12 @@ let ltac_call tac (args:glob_tactic_arg list) =
(* Calling a locally bound tactic *)
let ltac_lcall tac args =
- TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar(Loc.tag @@ Id.of_string tac),args)))
+ TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar CAst.(make @@ Id.of_string tac),args)))
let ltac_apply (f : Value.t) (args: Tacinterp.Value.t list) =
let fold arg (i, vars, lfun) =
let id = Id.of_string ("x" ^ string_of_int i) in
- let x = Reference (ArgVar (Loc.tag id)) in
+ let x = Reference (ArgVar CAst.(make id)) in
(succ i, x :: vars, Id.Map.add id arg lfun)
in
let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in
@@ -206,7 +206,7 @@ let get_res =
let exec_tactic env evd n f args =
let fold arg (i, vars, lfun) =
let id = Id.of_string ("x" ^ string_of_int i) in
- let x = Reference (ArgVar (Loc.tag id)) in
+ let x = Reference (ArgVar CAst.(make id)) in
(succ i, x :: vars, Id.Map.add id (Value.of_constr arg) lfun)
in
let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 499154d50..4ae746288 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -268,7 +268,7 @@ let interp_wit wit ist gl x =
sigma, Tacinterp.Value.cast (topwit wit) arg
let interp_hyp ist gl (SsrHyp (loc, id)) =
- let s, id' = interp_wit wit_var ist gl (loc, id) in
+ let s, id' = interp_wit wit_var ist gl CAst.(make ?loc id) in
if not_section_id id' then s, SsrHyp (loc, id') else
hyp_err ?loc "Can't clear section hypothesis " id'
@@ -835,9 +835,9 @@ let rec mkCHoles ?loc n =
if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) :: mkCHoles ?loc (n - 1)
let mkCHole loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None)
let mkCLambda ?loc name ty t = CAst.make ?loc @@
- CLambdaN ([CLocalAssum([loc, name], Default Explicit, ty)], t)
+ CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t)
let mkCArrow ?loc ty t = CAst.make ?loc @@
- CProdN ([CLocalAssum([Loc.tag Anonymous], Default Explicit, ty)], t)
+ CProdN ([CLocalAssum([CAst.make Anonymous], Default Explicit, ty)], t)
let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, CastConv ty)
let rec isCHoles = function { CAst.v = CHole _ } :: cl -> isCHoles cl | cl -> cl = []
@@ -855,7 +855,7 @@ let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty =
| _, (_, Some ty) ->
let rec force_type ty = CAst.(map (function
| CProdN (abs, t) ->
- n_binders := !n_binders + List.length (List.flatten (List.map (function CLocalAssum (nal,_,_) -> nal | CLocalDef (na,_,_) -> [na] | CLocalPattern (_,_) -> (* We count a 'pat for 1; TO BE CHECKED *) [Loc.tag Name.Anonymous]) abs));
+ n_binders := !n_binders + List.length (List.flatten (List.map (function CLocalAssum (nal,_,_) -> nal | CLocalDef (na,_,_) -> [na] | CLocalPattern _ -> (* We count a 'pat for 1; TO BE CHECKED *) [CAst.make Name.Anonymous]) abs));
CProdN (abs, force_type t)
| CLetIn (n, v, oty, t) -> incr n_binders; CLetIn (n, v, oty, force_type t)
| _ -> (mkCCast ty (mkCType None)).v)) ty in
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 211cad3f5..0d8044f19 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -130,7 +130,7 @@ let pr_ssrhyp _ _ _ = pr_hyp
let wit_ssrhyprep = add_genarg "ssrhyprep" pr_hyp
let intern_hyp ist (SsrHyp (loc, id) as hyp) =
- let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) (loc, id)) in
+ let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) CAst.(make ?loc id)) in
if not_section_id id then hyp else
hyp_err ?loc "Can't clear section hypothesis " id
@@ -316,7 +316,7 @@ END
let pr_index = function
- | Misctypes.ArgVar (_, id) -> pr_id id
+ | Misctypes.ArgVar {CAst.v=id} -> pr_id id
| Misctypes.ArgArg n when n > 0 -> int n
| _ -> mt ()
let pr_ssrindex _ _ _ = pr_index
@@ -330,13 +330,13 @@ let mk_index ?loc = function
| iv -> iv
let interp_index ist gl idx =
- Tacmach.project gl,
+ Tacmach.project gl,
match idx with
| Misctypes.ArgArg _ -> idx
- | Misctypes.ArgVar (loc, id) ->
+ | Misctypes.ArgVar id ->
let i =
try
- let v = Id.Map.find id ist.Tacinterp.lfun in
+ let v = Id.Map.find id.CAst.v ist.Tacinterp.lfun in
begin match Tacinterp.Value.to_int v with
| Some i -> i
| None ->
@@ -350,8 +350,8 @@ let interp_index ist gl idx =
end
| None -> raise Not_found
end end
- with _ -> CErrors.user_err ?loc (str"Index not a number") in
- Misctypes.ArgArg (check_index ?loc i)
+ with _ -> CErrors.user_err ?loc:id.CAst.loc (str"Index not a number") in
+ Misctypes.ArgArg (check_index ?loc:id.CAst.loc i)
open Pltac
@@ -1014,22 +1014,22 @@ let rec mkBstruct i = function
| [] -> []
let rec format_local_binders h0 bl0 = match h0, bl0 with
- | BFvar :: h, CLocalAssum ([_, x], _, _) :: bl ->
+ | BFvar :: h, CLocalAssum ([{CAst.v=x}], _, _) :: bl ->
Bvar x :: format_local_binders h bl
| BFdecl _ :: h, CLocalAssum (lxs, _, t) :: bl ->
- Bdecl (List.map snd lxs, t) :: format_local_binders h bl
- | BFdef :: h, CLocalDef ((_, x), v, oty) :: bl ->
+ Bdecl (List.map (fun x -> x.CAst.v) lxs, t) :: format_local_binders h bl
+ | BFdef :: h, CLocalDef ({CAst.v=x}, v, oty) :: bl ->
Bdef (x, oty, v) :: format_local_binders h bl
| _ -> []
let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with
- | BFvar :: h, { v = CLambdaN ([CLocalAssum([_, x], _, _)], c) } ->
+ | BFvar :: h, { v = CLambdaN ([CLocalAssum([{CAst.v=x}], _, _)], c) } ->
let bs, c' = format_constr_expr h c in
Bvar x :: bs, c'
| BFdecl _:: h, { v = CLambdaN ([CLocalAssum(lxs, _, t)], c) } ->
let bs, c' = format_constr_expr h c in
- Bdecl (List.map snd lxs, t) :: bs, c'
- | BFdef :: h, { v = CLetIn((_, x), v, oty, c) } ->
+ Bdecl (List.map (fun x -> x.CAst.v) lxs, t) :: bs, c'
+ | BFdef :: h, { v = CLetIn({CAst.v=x}, v, oty, c) } ->
let bs, c' = format_constr_expr h c in
Bdef (x, oty, v) :: bs, c'
| [BFcast], { v = CCast (c, CastConv t) } ->
@@ -1037,7 +1037,7 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with
| BFrec (has_str, has_cast) :: h,
{ v = CFix ( _, [_, (Some locn, CStructRec), bl, t, c]) } ->
let bs = format_local_binders h bl in
- let bstr = if has_str then [Bstruct (Name (snd locn))] else [] in
+ let bstr = if has_str then [Bstruct (Name locn.CAst.v)] else [] in
bs @ bstr @ (if has_cast then [Bcast t] else []), c
| BFrec (_, has_cast) :: h, { v = CCoFix ( _, [_, bl, t, c]) } ->
format_local_binders h bl @ (if has_cast then [Bcast t] else []), c
@@ -1156,18 +1156,18 @@ ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY pr_ssrbvar
END
let bvar_lname = let open CAst in function
- | { v = CRef (Ident (loc, id), _) } -> Loc.tag ?loc @@ Name id
- | { loc = loc } -> Loc.tag ?loc Anonymous
+ | { v = CRef (Ident (loc, id), _) } -> CAst.make ?loc @@ Name id
+ | { loc = loc } -> CAst.make ?loc Anonymous
let pr_ssrbinder prc _ _ (_, c) = prc c
ARGUMENT EXTEND ssrbinder TYPED AS ssrfwdfmt * constr PRINTED BY pr_ssrbinder
| [ ssrbvar(bv) ] ->
- [ let xloc, _ as x = bvar_lname bv in
+ [ let { CAst.loc=xloc } as x = bvar_lname bv in
(FwdPose, [BFvar]),
CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) ]
| [ "(" ssrbvar(bv) ")" ] ->
- [ let xloc, _ as x = bvar_lname bv in
+ [ let { CAst.loc=xloc } as x = bvar_lname bv in
(FwdPose, [BFvar]),
CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) ]
| [ "(" ssrbvar(bv) ":" lconstr(t) ")" ] ->
@@ -1191,7 +1191,7 @@ GEXTEND Gram
[ ["of" | "&"]; c = operconstr LEVEL "99" ->
let loc = !@loc in
(FwdPose, [BFvar]),
- CAst.make ~loc @@ CLambdaN ([CLocalAssum ([Loc.tag ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) ]
+ CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) ]
];
END
@@ -1250,13 +1250,13 @@ END
let pr_ssrfixfwd _ _ _ (id, fwd) = str " fix " ++ pr_id id ++ pr_fwd fwd
let bvar_locid = function
- | { CAst.v = CRef (Ident (loc, id), _) } -> loc, id
+ | { CAst.v = CRef (Ident (loc, id), _) } -> CAst.make ?loc id
| _ -> CErrors.user_err (Pp.str "Missing identifier after \"(co)fix\"")
ARGUMENT EXTEND ssrfixfwd TYPED AS ident * ssrfwd PRINTED BY pr_ssrfixfwd
| [ "fix" ssrbvar(bv) ssrbinder_list(bs) ssrstruct(sid) ssrfwd(fwd) ] ->
- [ let (_, id) as lid = bvar_locid bv in
+ [ let { CAst.v=id } as lid = bvar_locid bv in
let (fk, h), (ck, (rc, oc)) = fwd in
let c = Option.get oc in
let has_cast, t', c' = match format_constr_expr h c with
@@ -1265,8 +1265,10 @@ ARGUMENT EXTEND ssrfixfwd TYPED AS ident * ssrfwd PRINTED BY pr_ssrfixfwd
let lb = fix_binders bs in
let has_struct, i =
let rec loop = function
- (l', Name id') :: _ when Option.equal Id.equal sid (Some id') -> true, (l', id')
- | [l', Name id'] when sid = None -> false, (l', id')
+ | {CAst.loc=l'; v=Name id'} :: _ when Option.equal Id.equal sid (Some id') ->
+ true, CAst.make ?loc:l' id'
+ | [{CAst.loc=l';v=Name id'}] when sid = None ->
+ false, CAst.make ?loc:l' id'
| _ :: bn -> loop bn
| [] -> CErrors.user_err (Pp.str "Bad structural argument") in
loop (names_of_local_assums lb) in
@@ -1282,7 +1284,7 @@ let pr_ssrcofixfwd _ _ _ (id, fwd) = str " cofix " ++ pr_id id ++ pr_fwd fwd
ARGUMENT EXTEND ssrcofixfwd TYPED AS ssrfixfwd PRINTED BY pr_ssrcofixfwd
| [ "cofix" ssrbvar(bv) ssrbinder_list(bs) ssrfwd(fwd) ] ->
- [ let _, id as lid = bvar_locid bv in
+ [ let { CAst.v=id } as lid = bvar_locid bv in
let (fk, h), (ck, (rc, oc)) = fwd in
let c = Option.get oc in
let has_cast, t', c' = match format_constr_expr h c with
@@ -1323,7 +1325,7 @@ END
let intro_id_to_binder = List.map (function
| IPatId id ->
- let xloc, _ as x = bvar_lname (mkCVar id) in
+ let { CAst.loc=xloc } as x = bvar_lname (mkCVar id) in
(FwdPose, [BFvar]),
CAst.make @@ CLambdaN ([CLocalAssum([x], Default Explicit, mkCHole xloc)],
mkCHole None)
@@ -1332,9 +1334,9 @@ let intro_id_to_binder = List.map (function
let binder_to_intro_id = CAst.(List.map (function
| (FwdPose, [BFvar]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) }
| (FwdPose, [BFdecl _]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) } ->
- List.map (function (_, Name id) -> IPatId id | _ -> IPatAnon One) ids
- | (FwdPose, [BFdef]), { v = CLetIn ((_,Name id),_,_,_) } -> [IPatId id]
- | (FwdPose, [BFdef]), { v = CLetIn ((_,Anonymous),_,_,_) } -> [IPatAnon One]
+ List.map (function {v=Name id} -> IPatId id | _ -> IPatAnon One) ids
+ | (FwdPose, [BFdef]), { v = CLetIn ({v=Name id},_,_,_) } -> [IPatId id]
+ | (FwdPose, [BFdef]), { v = CLetIn ({v=Anonymous},_,_,_) } -> [IPatAnon One]
| _ -> anomaly "ssrbinder is not a binder"))
let pr_ssrhavefwdwbinders _ _ prt (tr,((hpats, (fwd, hint)))) =
@@ -1405,7 +1407,7 @@ let ssrorelse = Gram.entry_create "ssrorelse"
GEXTEND Gram
GLOBAL: ssrorelse ssrseqarg;
ssrseqidx: [
- [ test_ssrseqvar; id = Prim.ident -> ArgVar (Loc.tag ~loc:!@loc id)
+ [ test_ssrseqvar; id = Prim.ident -> ArgVar (CAst.make ~loc:!@loc id)
| n = Prim.natural -> ArgArg (check_index ~loc:!@loc n)
] ];
ssrswap: [[ IDENT "first" -> !@loc, true | IDENT "last" -> !@loc, false ]];
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 25d1472f1..8e6e0347f 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -79,9 +79,9 @@ let aliasvar = function
let mk_cnotype mp = aliasvar mp, None in
let mk_ctype mp t = aliasvar mp, Some t in
let mk_rtype t = Some t in
-let mk_dthen ?loc (mp, ct, rt) c = (Loc.tag ?loc (mp, c)), ct, rt in
+let mk_dthen ?loc (mp, ct, rt) c = (CAst.make ?loc (mp, c)), ct, rt in
let mk_let ?loc rt ct mp c1 =
- CAst.make ?loc @@ CCases (LetPatternStyle, rt, ct, [Loc.tag ?loc (mp, c1)]) in
+ CAst.make ?loc @@ CCases (LetPatternStyle, rt, ct, [CAst.make ?loc (mp, c1)]) in
let mk_pat c (na, t) = (c, na, t) in
GEXTEND Gram
GLOBAL: binder_constr;
@@ -94,14 +94,16 @@ GEXTEND Gram
] ];
ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> mk_dthen ~loc:!@loc dp c ]];
ssr_elsepat: [[ "else" -> [[CAst.make ~loc:!@loc @@ CPatAtom None]] ]];
- ssr_else: [[ mp = ssr_elsepat; c = lconstr -> Loc.tag ~loc:!@loc (mp, c) ]];
+ ssr_else: [[ mp = ssr_elsepat; c = lconstr -> CAst.make ~loc:!@loc (mp, c) ]];
binder_constr: [
[ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else ->
let b1, ct, rt = db1 in CAst.make ~loc:!@loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2])
| "if"; c = operconstr LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else ->
let b1, ct, rt = db1 in
- let b1, b2 =
- let (l1, (p1, r1)), (l2, (p2, r2)) = b1, b2 in (l1, (p1, r2)), (l2, (p2, r1)) in
+ let b1, b2 = let open CAst in
+ let {loc=l1; v=(p1, r1)}, {loc=l2; v=(p2, r2)} = b1, b2 in
+ (make ?loc:l1 (p1, r2), make ?loc:l2 (p2, r1))
+ in
CAst.make ~loc:!@loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2])
| "let"; ":"; mp = ssr_mpat; ":="; c = lconstr; "in"; c1 = lconstr ->
mk_let ~loc:!@loc no_rt [mk_pat c no_ct] mp c1
@@ -118,7 +120,7 @@ GEXTEND Gram
GLOBAL: closed_binder;
closed_binder: [
[ ["of" | "&"]; c = operconstr LEVEL "99" ->
- [CLocalAssum ([Loc.tag ~loc:!@loc Anonymous], Default Explicit, c)]
+ [CLocalAssum ([CAst.make ~loc:!@loc Anonymous], Default Explicit, c)]
] ];
END
(* }}} *)
@@ -553,7 +555,7 @@ GEXTEND Gram
let s = coerce_reference_to_id qid in
Vernacexpr.VernacDefinition
((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure),
- ((Loc.tag (Name s)),None), d)
+ ((CAst.make (Name s)),None), d)
]];
END
@@ -584,10 +586,10 @@ END
GEXTEND Gram
GLOBAL: hloc;
hloc: [
- [ "in"; "("; "Type"; "of"; id = ident; ")" ->
- Tacexpr.HypLocation ((Loc.tag id), Locus.InHypTypeOnly)
- | "in"; "("; IDENT "Value"; "of"; id = ident; ")" ->
- Tacexpr.HypLocation ((Loc.tag id), Locus.InHypValueOnly)
+ [ "in"; "("; "Type"; "of"; id = ident; ")" ->
+ Tacexpr.HypLocation (CAst.make id, Locus.InHypTypeOnly)
+ | "in"; "("; IDENT "Value"; "of"; id = ident; ")" ->
+ Tacexpr.HypLocation (CAst.make id, Locus.InHypValueOnly)
] ];
END
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 71e8b4ac4..73e212365 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -137,9 +137,9 @@ let destGLambda c = match DAst.get c with GLambda (Name id, _, _, c) -> (id, c)
let isGHole c = match DAst.get c with GHole _ -> true | _ -> false
let mkCHole ~loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None)
let mkCLambda ?loc name ty t = CAst.make ?loc @@
- CLambdaN ([CLocalAssum([Loc.tag ?loc name], Default Explicit, ty)], t)
+ CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t)
let mkCLetIn ?loc name bo t = CAst.make ?loc @@
- CLetIn ((Loc.tag ?loc name), bo, None, t)
+ CLetIn ((CAst.make ?loc name), bo, None, t)
let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty)
(** Constructors for rawconstr *)
let mkRHole = DAst.make @@ GHole (InternalHole, IntroAnonymous, None)