aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-02-24 09:26:03 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-02-24 09:26:03 +0100
commit7895d276146496648d576914aab4aded4b4a32cd (patch)
tree24e8de17078242c1ea39e31ecfe55a1c024d0eff
parent0c5f0afffd37582787f79267d9841259095b7edc (diff)
parent9bebbb96e58b3c1b0f7f88ba2af45462eae69b0f (diff)
Merge PR #6745: [ast] Improve precision of Ast location recognition in serialization.
-rw-r--r--dev/ci/user-overlays/06745-ejgallego-located+vernac.sh13
-rw-r--r--dev/doc/changes.md8
-rw-r--r--engine/evd.ml2
-rw-r--r--engine/evd.mli2
-rw-r--r--engine/uState.ml6
-rw-r--r--engine/uState.mli2
-rw-r--r--engine/universes.ml4
-rw-r--r--engine/universes.mli2
-rw-r--r--interp/constrexpr_ops.ml119
-rw-r--r--interp/constrexpr_ops.mli17
-rw-r--r--interp/constrextern.ml52
-rw-r--r--interp/constrintern.ml152
-rw-r--r--interp/constrintern.mli2
-rw-r--r--interp/declare.ml2
-rw-r--r--interp/declare.mli2
-rw-r--r--interp/dumpglob.ml6
-rw-r--r--interp/dumpglob.mli2
-rw-r--r--interp/implicit_quantifiers.ml32
-rw-r--r--interp/implicit_quantifiers.mli9
-rw-r--r--interp/reserve.ml2
-rw-r--r--interp/reserve.mli3
-rw-r--r--interp/stdarg.mli6
-rw-r--r--interp/topconstr.mli3
-rw-r--r--intf/constrexpr.ml28
-rw-r--r--intf/genredexpr.ml4
-rw-r--r--intf/misctypes.ml14
-rw-r--r--intf/vernacexpr.ml42
-rw-r--r--library/declaremods.ml5
-rw-r--r--library/declaremods.mli2
-rw-r--r--parsing/egramcoq.ml4
-rw-r--r--parsing/g_constr.ml450
-rw-r--r--parsing/g_prim.ml414
-rw-r--r--parsing/g_proofs.ml42
-rw-r--r--parsing/g_vernac.ml436
-rw-r--r--parsing/pcoq.mli18
-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
-rw-r--r--pretyping/univdecls.ml7
-rw-r--r--pretyping/univdecls.mli2
-rw-r--r--printing/ppconstr.ml55
-rw-r--r--printing/ppconstr.mli7
-rw-r--r--printing/pputils.ml4
-rw-r--r--printing/pputils.mli1
-rw-r--r--printing/ppvernac.ml46
-rw-r--r--printing/prettyp.mli4
-rw-r--r--printing/printmod.mli2
-rw-r--r--proofs/proof_global.ml2
-rw-r--r--proofs/proof_global.mli2
-rw-r--r--stm/stm.ml12
-rw-r--r--stm/vernac_classifier.ml44
-rw-r--r--tactics/equality.ml2
-rw-r--r--tactics/tactics.ml4
-rw-r--r--toplevel/vernac.ml2
-rw-r--r--vernac/classes.ml4
-rw-r--r--vernac/comAssumption.ml12
-rw-r--r--vernac/comAssumption.mli2
-rw-r--r--vernac/comFixpoint.ml8
-rw-r--r--vernac/comFixpoint.mli2
-rw-r--r--vernac/comInductive.ml10
-rw-r--r--vernac/comProgramFixpoint.ml8
-rw-r--r--vernac/indschemes.ml24
-rw-r--r--vernac/indschemes.mli7
-rw-r--r--vernac/lemmas.ml6
-rw-r--r--vernac/metasyntax.ml22
-rw-r--r--vernac/metasyntax.mli1
-rw-r--r--vernac/obligations.ml6
-rw-r--r--vernac/obligations.mli4
-rw-r--r--vernac/proof_using.ml2
-rw-r--r--vernac/record.ml17
-rw-r--r--vernac/vernacentries.ml63
-rw-r--r--vernac/vernacprop.ml12
95 files changed, 799 insertions, 755 deletions
diff --git a/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh b/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh
new file mode 100644
index 000000000..d1d61fec2
--- /dev/null
+++ b/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh
@@ -0,0 +1,13 @@
+if [ "$CI_PULL_REQUEST" = "6745" ] || [ "$CI_BRANCH" = "located+vernac" ]; then
+ ltac2_CI_BRANCH=located+vernac
+ ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+ Equations_CI_BRANCH=located+vernac
+ Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+ fiat_parsers_CI_BRANCH=located+vernac
+ fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat
+
+ Elpi_CI_BRANCH=located+vernac
+ Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 16a31790a..ab78b0956 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -49,6 +49,14 @@ We changed the type of the following functions:
a functional way. The old style of passing `evar_map`s as references
is not supported anymore.
+Changes in the abstract syntax tree:
+
+- The practical totality of the AST has been nodified using
+ `CAst.t`. This means that all objects coming from parsing will be
+ indeed wrapped in a `CAst.t`. `Loc.located` is on its way to
+ deprecation. Some minor interfaces changes have resulted from
+ this.
+
We have changed the representation of the following types:
- `Lib.object_prefix` is now a record instead of a nested tuple.
diff --git a/engine/evd.ml b/engine/evd.ml
index 0e9472158..2142cee37 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -802,7 +802,7 @@ let make_evar_universe_context e l =
| None -> uctx
| Some us ->
List.fold_left
- (fun uctx (loc,id) ->
+ (fun uctx { CAst.loc; v = id } ->
fst (UState.new_univ_variable ?loc univ_rigid (Some id) uctx))
uctx us
diff --git a/engine/evd.mli b/engine/evd.mli
index b28ce2a62..84fa70ef2 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -506,7 +506,7 @@ val constrain_variables : Univ.LSet.t -> UState.t -> UState.t
val evar_universe_context_of_binders :
Universes.universe_binders -> UState.t
-val make_evar_universe_context : env -> (Id.t located) list option -> UState.t
+val make_evar_universe_context : env -> Misctypes.lident list option -> UState.t
val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map
(** Raises Not_found if not a name for a universe in this map. *)
val universe_of_name : evar_map -> Id.t -> Univ.Level.t
diff --git a/engine/uState.ml b/engine/uState.ml
index 4b650c9c9..625495866 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -282,7 +282,7 @@ let pr_uctx_level uctx l =
Libnames.pr_reference (reference_of_level uctx l)
type universe_decl =
- (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+ (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
let error_unbound_universes left uctx =
let open Univ in
@@ -305,7 +305,7 @@ let universe_context ~names ~extensible uctx =
let levels = ContextSet.levels uctx.uctx_local in
let newinst, left =
List.fold_right
- (fun (loc,id) (newinst, acc) ->
+ (fun { CAst.loc; v = id } (newinst, acc) ->
let l =
try UNameMap.find id (fst uctx.uctx_names)
with Not_found -> assert false
@@ -325,7 +325,7 @@ let check_universe_context_set ~names ~extensible uctx =
if extensible then ()
else
let open Univ in
- let left = List.fold_left (fun left (loc,id) ->
+ let left = List.fold_left (fun left { CAst.loc; v = id } ->
let l =
try UNameMap.find id (fst uctx.uctx_names)
with Not_found -> assert false
diff --git a/engine/uState.mli b/engine/uState.mli
index 6657d6047..5c85b2b84 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -132,7 +132,7 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
val normalize : t -> t
type universe_decl =
- (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+ (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
(** [check_univ_decl ctx decl]
diff --git a/engine/universes.ml b/engine/universes.ml
index 3a00f0fd1..f3660a559 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -92,14 +92,14 @@ let register_universe_binders ref ubinders =
if not (Id.Map.is_empty ubinders)
then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders))
-type univ_name_list = Name.t Loc.located list
+type univ_name_list = Misctypes.lname list
let universe_binders_with_opt_names ref levels = function
| None -> universe_binders_of_global ref
| Some udecl ->
if Int.equal(List.length levels) (List.length udecl)
then
- List.fold_left2 (fun acc (_,na) lvl -> match na with
+ List.fold_left2 (fun acc { CAst.v = na} lvl -> match na with
| Anonymous -> acc
| Name na -> Names.Id.Map.add na lvl acc)
empty_binders udecl levels
diff --git a/engine/universes.mli b/engine/universes.mli
index cb6e2ba1b..04586a6f8 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -35,7 +35,7 @@ val empty_binders : universe_binders
val register_universe_binders : Globnames.global_reference -> universe_binders -> unit
val universe_binders_of_global : Globnames.global_reference -> universe_binders
-type univ_name_list = Name.t Loc.located list
+type univ_name_list = Misctypes.lname list
(** [universe_binders_with_opt_names ref u l]
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 8aca6e333..d05e7d909 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -61,13 +61,13 @@ let explicitation_eq ex1 ex2 = match ex1, ex2 with
Id.equal id1 id2
| _ -> false
-let eq_located f (_, x) (_, y) = f x y
+let eq_ast f { CAst.v = x } { CAst.v = y } = f x y
let rec cases_pattern_expr_eq p1 p2 =
if CAst.(p1.v == p2.v) then true
else match CAst.(p1.v, p2.v) with
| CPatAlias(a1,i1), CPatAlias(a2,i2) ->
- Name.equal (snd i1) (snd i2) && cases_pattern_expr_eq a1 a2
+ eq_ast Name.equal i1 i2 && cases_pattern_expr_eq a1 a2
| CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) ->
eq_reference c1 c2 &&
Option.equal (List.equal cases_pattern_expr_eq) a1 a2 &&
@@ -106,10 +106,10 @@ let rec constr_expr_eq e1 e2 =
else match CAst.(e1.v, e2.v) with
| CRef (r1,u1), CRef (r2,u2) -> eq_reference r1 r2 && eq_universes u1 u2
| CFix(id1,fl1), CFix(id2,fl2) ->
- eq_located Id.equal id1 id2 &&
+ eq_ast Id.equal id1 id2 &&
List.equal fix_expr_eq fl1 fl2
| CCoFix(id1,fl1), CCoFix(id2,fl2) ->
- eq_located Id.equal id1 id2 &&
+ eq_ast Id.equal id1 id2 &&
List.equal cofix_expr_eq fl1 fl2
| CProdN(bl1,a1), CProdN(bl2,a2) ->
List.equal local_binder_eq bl1 bl2 &&
@@ -117,8 +117,8 @@ let rec constr_expr_eq e1 e2 =
| CLambdaN(bl1,a1), CLambdaN(bl2,a2) ->
List.equal local_binder_eq bl1 bl2 &&
constr_expr_eq a1 a2
- | CLetIn((_,na1),a1,t1,b1), CLetIn((_,na2),a2,t2,b2) ->
- Name.equal na1 na2 &&
+ | CLetIn(na1,a1,t1,b1), CLetIn(na2,a2,t2,b2) ->
+ eq_ast Name.equal na1 na2 &&
constr_expr_eq a1 a2 &&
Option.equal constr_expr_eq t1 t2 &&
constr_expr_eq b1 b2
@@ -141,14 +141,14 @@ let rec constr_expr_eq e1 e2 =
List.equal case_expr_eq a1 a2 &&
List.equal branch_expr_eq brl1 brl2
| CLetTuple (n1, (m1, e1), t1, b1), CLetTuple (n2, (m2, e2), t2, b2) ->
- List.equal (eq_located Name.equal) n1 n2 &&
- Option.equal (eq_located Name.equal) m1 m2 &&
+ List.equal (eq_ast Name.equal) n1 n2 &&
+ Option.equal (eq_ast Name.equal) m1 m2 &&
Option.equal constr_expr_eq e1 e2 &&
constr_expr_eq t1 t2 &&
constr_expr_eq b1 b2
| CIf (e1, (n1, r1), t1, f1), CIf (e2, (n2, r2), t2, f2) ->
constr_expr_eq e1 e2 &&
- Option.equal (eq_located Name.equal) n1 n2 &&
+ Option.equal (eq_ast Name.equal) n1 n2 &&
Option.equal constr_expr_eq r1 r2 &&
constr_expr_eq t1 t2 &&
constr_expr_eq f1 f2
@@ -181,28 +181,28 @@ let rec constr_expr_eq e1 e2 =
| CGeneralization _ | CDelimiters _ | CProj _), _ -> false
and args_eq (a1,e1) (a2,e2) =
- Option.equal (eq_located explicitation_eq) e1 e2 &&
+ Option.equal (eq_ast explicitation_eq) e1 e2 &&
constr_expr_eq a1 a2
and case_expr_eq (e1, n1, p1) (e2, n2, p2) =
constr_expr_eq e1 e2 &&
- Option.equal (eq_located Name.equal) n1 n2 &&
+ Option.equal (eq_ast Name.equal) n1 n2 &&
Option.equal cases_pattern_expr_eq p1 p2
-and branch_expr_eq (_, (p1, e1)) (_, (p2, e2)) =
+and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} =
List.equal (List.equal cases_pattern_expr_eq) p1 p2 &&
constr_expr_eq e1 e2
and fix_expr_eq (id1,(j1, r1),bl1,a1,b1) (id2,(j2, r2),bl2,a2,b2) =
- (eq_located Id.equal id1 id2) &&
- Option.equal (eq_located Id.equal) j1 j2 &&
+ (eq_ast Id.equal id1 id2) &&
+ Option.equal (eq_ast Id.equal) j1 j2 &&
recursion_order_expr_eq r1 r2 &&
List.equal local_binder_eq bl1 bl2 &&
constr_expr_eq a1 a2 &&
constr_expr_eq b1 b2
and cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) =
- (eq_located Id.equal id1 id2) &&
+ (eq_ast Id.equal id1 id2) &&
List.equal local_binder_eq bl1 bl2 &&
constr_expr_eq a1 a2 &&
constr_expr_eq b1 b2
@@ -216,10 +216,10 @@ and recursion_order_expr_eq r1 r2 = match r1, r2 with
and local_binder_eq l1 l2 = match l1, l2 with
| CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) ->
- eq_located Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2
+ eq_ast Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2
| CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) ->
(** Don't care about the [binder_kind] *)
- List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2
+ List.equal (eq_ast Name.equal) n1 n2 && constr_expr_eq e1 e2
| _ -> false
and constr_notation_substitution_eq (e1, el1, b1, bl1) (e2, el2, b2, bl2) =
@@ -244,12 +244,12 @@ and cast_expr_eq c1 c2 = match c1, c2 with
let constr_loc c = CAst.(c.loc)
let cases_pattern_expr_loc cp = CAst.(cp.loc)
-let local_binder_loc = function
- | CLocalAssum ((loc,_)::_,_,t)
- | CLocalDef ((loc,_),t,None) -> Loc.merge_opt loc (constr_loc t)
- | CLocalDef ((loc,_),b,Some t) -> Loc.merge_opt loc (Loc.merge_opt (constr_loc b) (constr_loc t))
+let local_binder_loc = let open CAst in function
+ | CLocalAssum ({ loc } ::_,_,t)
+ | CLocalDef ( { loc },t,None) -> Loc.merge_opt loc (constr_loc t)
+ | CLocalDef ( { loc },b,Some t) -> Loc.merge_opt loc (Loc.merge_opt (constr_loc b) (constr_loc t))
| CLocalAssum ([],_,_) -> assert false
- | CLocalPattern (loc,_) -> loc
+ | CLocalPattern { loc } -> loc
let local_binders_loc bll = match bll with
| [] -> None
@@ -257,9 +257,6 @@ let local_binders_loc bll = match bll with
(** Folds and maps *)
-(* Legacy functions *)
-let down_located f (_l, x) = f x
-
let is_constructor id =
try Globnames.isConstructRef
(Smartlocate.global_of_extended_global
@@ -269,7 +266,7 @@ let is_constructor id =
let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with
| CPatRecord l ->
List.fold_left (fun acc (r, cp) -> cases_pattern_fold_names f acc cp) a l
- | CPatAlias (pat,(loc,na)) -> Name.fold_right f na (cases_pattern_fold_names f a pat)
+ | CPatAlias (pat,{CAst.v=na}) -> Name.fold_right f na (cases_pattern_fold_names f a pat)
| CPatOr (patl) ->
List.fold_left (cases_pattern_fold_names f) a patl
| CPatCstr (_,patl1,patl2) ->
@@ -301,17 +298,17 @@ let ids_of_cases_tomatch tms =
(fun (_, ona, indnal) l ->
Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t)
indnal
- (Option.fold_right (down_located (Name.fold_right Id.Set.add)) ona l))
+ (Option.fold_right (CAst.with_val (Name.fold_right Id.Set.add)) ona l))
tms Id.Set.empty
-let rec fold_local_binders g f n acc b = function
+let rec fold_local_binders g f n acc b = let open CAst in function
| CLocalAssum (nal,bk,t)::l ->
- let nal = snd (List.split nal) in
+ let nal = List.(map (fun {v} -> v) nal) in
let n' = List.fold_right (Name.fold_right g) nal n in
f n (fold_local_binders g f n' acc b l) t
- | CLocalDef ((_,na),c,t)::l ->
+ | CLocalDef ( { v = na },c,t)::l ->
Option.fold_left (f n) (f n (fold_local_binders g f (Name.fold_right g na n) acc b l) c) t
- | CLocalPattern (_,(pat,t))::l ->
+ | CLocalPattern { v = pat,t }::l ->
let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in
Option.fold_left (f n) acc t
| [] ->
@@ -322,7 +319,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
| CApp ((_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
| CProdN (l,b) | CLambdaN (l,b) -> fold_local_binders g f n acc b l
| CLetIn (na,a,t,b) ->
- f (Name.fold_right g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b
+ f (Name.fold_right g (na.CAst.v) n) (Option.fold_left (f n) (f n acc a) t) b
| CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b
| CCast (a,CastCoerce) -> f n acc a
| CNotation (_,(l,ll,bl,bll)) ->
@@ -339,18 +336,18 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
let ids = ids_of_cases_tomatch al in
let acc = Option.fold_left (f (Id.Set.fold g ids n)) acc rtnpo in
let acc = List.fold_left (f n) acc (List.map (fun (fst,_,_) -> fst) al) in
- List.fold_right (fun (loc,(patl,rhs)) acc ->
+ List.fold_right (fun {CAst.v=(patl,rhs)} acc ->
let ids = ids_of_pattern_list patl in
f (Id.Set.fold g ids n) acc rhs) bl acc
| CLetTuple (nal,(ona,po),b,c) ->
- let n' = List.fold_right (down_located (Name.fold_right g)) nal n in
- f (Option.fold_right (down_located (Name.fold_right g)) ona n') (f n acc b) c
+ let n' = List.fold_right (CAst.with_val (Name.fold_right g)) nal n in
+ f (Option.fold_right (CAst.with_val (Name.fold_right 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_right g)) ona n)) acc po
+ (f (Option.fold_right (CAst.with_val (Name.fold_right g)) ona n)) acc po
| CFix (_,l) ->
- let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in
+ let n' = List.fold_right (fun ( { CAst.v = id },_,_,_,_) -> g id) l n in
List.fold_right (fun (_,(_,o),lb,t,c) acc ->
fold_local_binders g f n'
(fold_local_binders g f n acc t lb) c lb) l acc
@@ -369,18 +366,19 @@ let free_vars_of_constr_expr c =
let occur_var_constr_expr id c = Id.Set.mem id (free_vars_of_constr_expr c)
(* Used in correctness and interface *)
-let map_binder g e nal = List.fold_right (down_located (Name.fold_right g)) nal e
+let map_binder g e nal = List.fold_right (CAst.with_val (Name.fold_right g)) nal e
let map_local_binders f g e bl =
(* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
+ let open CAst in
let h (e,bl) = function
CLocalAssum(nal,k,ty) ->
(map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl)
- | CLocalDef((loc,na),c,ty) ->
- (Name.fold_right g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl)
- | CLocalPattern (loc,(pat,t)) ->
+ | CLocalDef( { loc ; v = na } as cna ,c,ty) ->
+ (Name.fold_right g na e, CLocalDef(cna,f e c,Option.map (f e) ty)::bl)
+ | CLocalPattern { loc; v = pat,t } ->
let ids = ids_of_pattern pat in
- (Id.Set.fold g ids e, CLocalPattern (loc,(pat,Option.map (f e) t))::bl) in
+ (Id.Set.fold g ids e, CLocalPattern (make ?loc (pat,Option.map (f e) t))::bl) in
let (e,rbl) = List.fold_left h (e,[]) bl in
(e, List.rev rbl)
@@ -393,7 +391,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function
| CLambdaN (bl,b) ->
let (e,bl) = map_local_binders f g e bl in CLambdaN (bl,f e b)
| CLetIn (na,a,t,b) ->
- CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (snd na) e) b)
+ CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (na.CAst.v) e) b)
| CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c)
| CNotation (n,(l,ll,bl,bll)) ->
(* This is an approximation because we don't know what binds what *)
@@ -405,32 +403,32 @@ let map_constr_expr_with_binders g f e = CAst.map (function
| CPrim _ | CRef _ as x -> x
| CRecord l -> CRecord (List.map (fun (id, c) -> (id, f e c)) l)
| CCases (sty,rtnpo,a,bl) ->
- let bl = List.map (fun (loc,(patl,rhs)) ->
+ let bl = List.map (fun {CAst.v=(patl,rhs);loc} ->
let ids = ids_of_pattern_list patl in
- (loc,(patl,f (Id.Set.fold g ids e) rhs))) bl in
+ CAst.make ?loc (patl,f (Id.Set.fold g ids e) rhs)) bl in
let ids = ids_of_cases_tomatch a in
let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in
CCases (sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl)
| CLetTuple (nal,(ona,po),b,c) ->
- let e' = List.fold_right (down_located (Name.fold_right g)) nal e in
- let e'' = Option.fold_right (down_located (Name.fold_right g)) ona e in
+ let e' = List.fold_right (CAst.with_val (Name.fold_right g)) nal e in
+ let e'' = Option.fold_right (CAst.with_val (Name.fold_right g)) ona e in
CLetTuple (nal,(ona,Option.map (f e'') po),f e b,f e' c)
| CIf (c,(ona,po),b1,b2) ->
- let e' = Option.fold_right (down_located (Name.fold_right g)) ona e in
+ let e' = Option.fold_right (CAst.with_val (Name.fold_right g)) ona e in
CIf (f e c,(ona,Option.map (f e') po),f e b1,f e b2)
| CFix (id,dl) ->
CFix (id,List.map (fun (id,n,bl,t,d) ->
let (e',bl') = map_local_binders f g e bl in
let t' = f e' t in
(* Note: fix names should be inserted before the arguments... *)
- let e'' = List.fold_left (fun e ((_,id),_,_,_,_) -> g id e) e' dl in
+ let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_,_) -> g id e) e' dl in
let d' = f e'' d in
(id,n,bl',t',d')) dl)
| CCoFix (id,dl) ->
CCoFix (id,List.map (fun (id,bl,t,d) ->
let (e',bl') = map_local_binders f g e bl in
let t' = f e' t in
- let e'' = List.fold_left (fun e ((_,id),_,_,_) -> g id e) e' dl in
+ let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_) -> g id e) e' dl in
let d' = f e'' d in
(id,bl',t',d')) dl)
| CProj (p,c) ->
@@ -471,17 +469,18 @@ let error_invalid_pattern_notation ?loc () =
(* Interpret the index of a recursion order annotation *)
let split_at_annot bl na =
- let names = List.map snd (names_of_local_assums bl) in
+ let open CAst in
+ let names = List.map (fun { v } -> v) (names_of_local_assums bl) in
match na with
| None ->
begin match names with
| [] -> CErrors.user_err (Pp.str "A fixpoint needs at least one parameter.")
| _ -> ([], bl)
end
- | Some (loc, id) ->
+ | Some { loc; v = id } ->
let rec aux acc = function
| CLocalAssum (bls, k, t) as x :: rest ->
- let test (_, na) = match na with
+ let test { CAst.v = na } = match na with
| Name id' -> Id.equal id id'
| Anonymous -> false
in
@@ -495,13 +494,13 @@ let split_at_annot bl na =
in
(List.rev ans, CLocalAssum (r, k, t) :: rest)
end
- | CLocalDef ((_,na),_,_) as x :: rest ->
+ | CLocalDef ({ CAst.v = na },_,_) as x :: rest ->
if Name.equal (Name id) na then
CErrors.user_err ?loc
(Id.print id ++ str" must be a proper parameter and not a local definition.")
else
aux (x :: acc) rest
- | CLocalPattern (_,_) :: rest ->
+ | CLocalPattern _ :: rest ->
Loc.raise ?loc (Stream.Error "pattern with quote not allowed after fix")
| [] ->
CErrors.user_err ?loc
@@ -536,14 +535,14 @@ let coerce_reference_to_id = function
(str "This expression should be a simple identifier.")
let coerce_to_id = function
- | { CAst.v = CRef (Ident (loc,id),None) } -> (loc,id)
+ | { CAst.v = CRef (Ident (loc,id),None) } -> CAst.make ?loc id
| { CAst.loc; _ } -> CErrors.user_err ?loc
~hdr:"coerce_to_id"
(str "This expression should be a simple identifier.")
let coerce_to_name = function
- | { CAst.v = CRef (Ident (loc,id),None) } -> (loc,Name id)
- | { CAst.loc; CAst.v = CHole (None,Misctypes.IntroAnonymous,None) } -> (loc,Anonymous)
+ | { CAst.v = CRef (Ident (loc,id),None) } -> CAst.make ?loc @@ Name id
+ | { CAst.loc; CAst.v = CHole (None,Misctypes.IntroAnonymous,None) } -> CAst.make ?loc Anonymous
| { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name"
(str "This expression should be a name.")
@@ -569,8 +568,8 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function
CPatAtom (Some r)
| CHole (None,Misctypes.IntroAnonymous,None) ->
CPatAtom None
- | CLetIn ((loc,Name id),b,None,{ CAst.v = CRef (Ident (_,id'),None) }) when Id.equal id id' ->
- CPatAlias (coerce_to_cases_pattern_expr b, (loc,Name id))
+ | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef (Ident (_,id'),None) }) when Id.equal id id' ->
+ CPatAlias (coerce_to_cases_pattern_expr b, CAst.(make ?loc @@ Name id))
| CApp ((None,p),args) when List.for_all (fun (_,e) -> e=None) args ->
(mkAppPattern (coerce_to_cases_pattern_expr p) (List.map (fun (a,_) -> coerce_to_cases_pattern_expr a) args)).CAst.v
| CAppExpl ((None,r,i),args) ->
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 0b00b0e4d..50c818d3c 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Loc
open Names
open Libnames
open Misctypes
@@ -44,9 +43,9 @@ val mkIdentC : Id.t -> constr_expr
val mkRefC : reference -> constr_expr
val mkAppC : constr_expr * constr_expr list -> constr_expr
val mkCastC : constr_expr * constr_expr cast_type -> constr_expr
-val mkLambdaC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr
-val mkLetInC : Name.t located * constr_expr * constr_expr option * constr_expr -> constr_expr
-val mkProdC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr
+val mkLambdaC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr
+val mkLetInC : lname * constr_expr * constr_expr option * constr_expr -> constr_expr
+val mkProdC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr
val mkCLambdaN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
(** Same as [abstract_constr_expr], with location *)
@@ -72,10 +71,10 @@ val prod_constr_expr : constr_expr -> local_binder_expr list -> constr_expr
val coerce_reference_to_id : reference -> Id.t
(** FIXME: nothing to do here *)
-val coerce_to_id : constr_expr -> Id.t located
+val coerce_to_id : constr_expr -> lident
(** Destruct terms of the form [CRef (Ident _)]. *)
-val coerce_to_name : constr_expr -> Name.t located
+val coerce_to_name : constr_expr -> lname
(** Destruct terms of the form [CRef (Ident _)] or [CHole _]. *)
val coerce_to_cases_pattern_expr : constr_expr -> cases_pattern_expr
@@ -84,10 +83,10 @@ val coerce_to_cases_pattern_expr : constr_expr -> cases_pattern_expr
val default_binder_kind : binder_kind
-val names_of_local_binders : local_binder_expr list -> Name.t located list
+val names_of_local_binders : local_binder_expr list -> lname list
(** Retrieve a list of binding names from a list of binders. *)
-val names_of_local_assums : local_binder_expr list -> Name.t located list
+val names_of_local_assums : local_binder_expr list -> lname list
(** Same as [names_of_local_binder_exprs], but does not take the [let] bindings into
account. *)
@@ -113,7 +112,7 @@ val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t
val free_vars_of_constr_expr : constr_expr -> Id.Set.t
val occur_var_constr_expr : Id.t -> constr_expr -> bool
-val split_at_annot : local_binder_expr list -> Id.t located option -> local_binder_expr list * local_binder_expr list
+val split_at_annot : local_binder_expr list -> lident option -> local_binder_expr list * local_binder_expr list
val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list
val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 9e18966b6..dec86ba81 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -257,7 +257,7 @@ let insert_pat_delimiters ?loc p = function
let insert_pat_alias ?loc p = function
| Anonymous -> p
- | Name _ as na -> CAst.make ?loc @@ CPatAlias (p,(loc,na))
+ | Name _ as na -> CAst.make ?loc @@ CPatAlias (p,(CAst.make ?loc na))
(**********************************************************************)
(* conversion of references *)
@@ -574,7 +574,7 @@ let explicitize inctx impl (cf,f) args =
is_significant_implicit (Lazy.force a))
in
if visible then
- (Lazy.force a,Some (Loc.tag @@ ExplByName (name_of_implicit imp))) :: tail
+ (Lazy.force a,Some (make @@ ExplByName (name_of_implicit imp))) :: tail
else
tail
| a::args, _::impl -> (Lazy.force a,None) :: exprec (q+1) (args,impl)
@@ -816,7 +816,7 @@ let rec extern inctx scopes vars r =
(List.map (fun c -> lazy (sub_extern true scopes vars c)) args))
| GLetIn (na,b,t,c) ->
- CLetIn ((loc,na),sub_extern false scopes vars b,
+ CLetIn (make ?loc na,sub_extern false scopes vars b,
Option.map (extern_typ scopes vars) t,
extern inctx scopes (add_vname vars na) c)
@@ -840,12 +840,12 @@ let rec extern inctx scopes vars r =
| None -> None
| Some ntn ->
if occur_glob_constr id ntn then
- Some (Loc.tag Anonymous)
+ Some (CAst.make Anonymous)
else None
end
| Anonymous, _ -> None
| Name id, GVar id' when Id.equal id id' -> None
- | Name _, _ -> Some (Loc.tag na) in
+ | Name _, _ -> Some (CAst.make na) in
(sub_extern false scopes vars tm,
na',
Option.map (fun (loc,(ind,nal)) ->
@@ -859,15 +859,15 @@ let rec extern inctx scopes vars r =
CCases (sty,rtntypopt',tml,eqns)
| GLetTuple (nal,(na,typopt),tm,b) ->
- CLetTuple (List.map (fun na -> (Loc.tag na)) nal,
- (Option.map (fun _ -> (Loc.tag na)) typopt,
+ CLetTuple (List.map CAst.make nal,
+ (Option.map (fun _ -> (make 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 (c,(na,typopt),b1,b2) ->
CIf (sub_extern false scopes vars c,
- (Option.map (fun _ -> (Loc.tag na)) typopt,
+ (Option.map (fun _ -> (CAst.make na)) typopt,
Option.map (extern_typ scopes (add_vname vars na)) typopt),
sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2)
@@ -885,13 +885,13 @@ let rec extern inctx scopes vars r =
let n =
match fst nv.(i) with
| None -> None
- | Some x -> Some (Loc.tag @@ Name.get_id (List.nth assums x))
+ | Some x -> Some (CAst.make @@ Name.get_id (List.nth assums x))
in
let ro = extern_recursion_order scopes vars (snd nv.(i)) in
- ((Loc.tag fi), (n, ro), bl, extern_typ scopes vars0 ty,
+ ((CAst.make fi), (n, ro), bl, extern_typ scopes vars0 ty,
extern false scopes vars1 def)) idv
in
- CFix ((loc,idv.(n)),Array.to_list listdecl)
+ CFix (CAst.(make ?loc idv.(n)), Array.to_list listdecl)
| GCoFix n ->
let listdecl =
Array.mapi (fun i fi ->
@@ -899,10 +899,10 @@ let rec extern inctx scopes vars r =
let (_,ids,bl) = extern_local_binder scopes vars bl in
let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in
let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in
- ((Loc.tag fi),bl,extern_typ scopes vars0 tyv.(i),
+ ((CAst.make fi),bl,extern_typ scopes vars0 tyv.(i),
sub_extern false scopes vars1 bv.(i))) idv
in
- CCoFix ((loc,idv.(n)),Array.to_list listdecl))
+ CCoFix (CAst.(make ?loc idv.(n)),Array.to_list listdecl))
| GSort s -> CSort (extern_glob_sort s)
@@ -932,7 +932,7 @@ and factorize_prod scopes vars na bk aty c =
let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in
let b = extern_typ scopes vars b in
let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in
- let binder = CLocalPattern (c.loc,(p,None)) in
+ let binder = CLocalPattern (make ?loc:c.loc (p,None)) in
(match b.v with
| CProdN (bl,b) -> CProdN (binder::bl,b)
| _ -> CProdN ([binder],b))
@@ -943,11 +943,11 @@ and factorize_prod scopes vars na bk aty c =
| Name id, CProdN (CLocalAssum(nal,Default bk',ty)::bl,b)
when binding_kind_eq bk bk' && constr_expr_eq aty ty
&& not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) ->
- CProdN (CLocalAssum(Loc.tag na::nal,Default bk,aty)::bl,b)
+ CProdN (CLocalAssum(make na::nal,Default bk,aty)::bl,b)
| _, CProdN (bl,b) ->
- CProdN (CLocalAssum([Loc.tag na],Default bk,aty)::bl,b)
+ CProdN (CLocalAssum([make na],Default bk,aty)::bl,b)
| _, _ ->
- CProdN ([CLocalAssum([Loc.tag na],Default bk,aty)],c)
+ CProdN ([CLocalAssum([make na],Default bk,aty)],c)
and factorize_lambda inctx scopes vars na bk aty c =
let store, get = set_temporary_memory () in
@@ -960,7 +960,7 @@ and factorize_lambda inctx scopes vars na bk aty c =
let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in
let b = sub_extern inctx scopes vars b in
let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in
- let binder = CLocalPattern (c.loc,(p,None)) in
+ let binder = CLocalPattern (make ?loc:c.loc (p,None)) in
(match b.v with
| CLambdaN (bl,b) -> CLambdaN (binder::bl,b)
| _ -> CLambdaN ([binder],b))
@@ -971,11 +971,11 @@ and factorize_lambda inctx scopes vars na bk aty c =
| CLambdaN (CLocalAssum(nal,Default bk',ty)::bl,b)
when binding_kind_eq bk bk' && constr_expr_eq aty ty
&& not (occur_name na ty) (* avoid na in ty escapes scope *) ->
- CLambdaN (CLocalAssum(Loc.tag na::nal,Default bk,aty)::bl,b)
+ CLambdaN (CLocalAssum(make na::nal,Default bk,aty)::bl,b)
| CLambdaN (bl,b) ->
- CLambdaN (CLocalAssum([Loc.tag na],Default bk,aty)::bl,b)
+ CLambdaN (CLocalAssum([make na],Default bk,aty)::bl,b)
| _ ->
- CLambdaN ([CLocalAssum([Loc.tag na],Default bk,aty)],c)
+ CLambdaN ([CLocalAssum([make na],Default bk,aty)],c)
and extern_local_binder scopes vars = function
[] -> ([],[],[])
@@ -985,7 +985,7 @@ and extern_local_binder scopes vars = function
let (assums,ids,l) =
extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l in
(assums,na::ids,
- CLocalDef((Loc.tag na), extern false scopes vars bd,
+ CLocalDef(CAst.make na, extern false scopes vars bd,
Option.map (extern false scopes vars) ty) :: l)
| GLocalAssum (na,bk,ty) ->
@@ -996,21 +996,21 @@ and extern_local_binder scopes vars = function
match na with Name id -> not (occur_var_constr_expr id ty')
| _ -> true ->
(na::assums,na::ids,
- CLocalAssum((Loc.tag na)::nal,k,ty')::l)
+ CLocalAssum(CAst.make na::nal,k,ty')::l)
| (assums,ids,l) ->
(na::assums,na::ids,
- CLocalAssum([(Loc.tag na)],Default bk,ty) :: l))
+ CLocalAssum([CAst.make na],Default bk,ty) :: l))
| GLocalPattern ((p,_),_,bk,ty) ->
let ty =
if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in
let p = mkCPatOr (List.map (extern_cases_pattern vars) p) in
let (assums,ids,l) = extern_local_binder scopes vars l in
- (assums,ids, CLocalPattern(Loc.tag @@ (p,ty)) :: l)
+ (assums,ids, CLocalPattern(CAst.make @@ (p,ty)) :: l)
and extern_eqn inctx scopes vars (loc,(ids,pll,c)) =
let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in
- Loc.tag ?loc (pll,extern inctx scopes vars c)
+ make ?loc (pll,extern inctx scopes vars c)
and extern_notation (tmp_scope,scopes as allscopes) vars t = function
| [] -> raise No_match
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 694bec897..d03aa3552 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -9,6 +9,7 @@
open Pp
open CErrors
open Util
+open CAst
open Names
open Nameops
open Namegen
@@ -328,8 +329,8 @@ let impls_term_list ?(args = []) =
in aux []
(* Check if in binder "(x1 x2 .. xn : t)", none of x1 .. xn-1 occurs in t *)
-let rec check_capture ty = function
- | (loc,Name id)::(_,Name id')::_ when occur_glob_constr id ty ->
+let rec check_capture ty = let open CAst in function
+ | { loc; v = Name id } :: { v = Name id' } :: _ when occur_glob_constr id ty ->
raise (InternalizationError (loc,VariableCapture (id,id')))
| _::nal ->
check_capture ty nal
@@ -360,22 +361,23 @@ let check_hidden_implicit_parameters ?loc id impls =
strbrk "the type of a constructor shall use a different name.")
let push_name_env ?(global_level=false) ntnvars implargs env =
+ let open CAst in
function
- | loc,Anonymous ->
+ | { loc; v = Anonymous } ->
if global_level then
user_err ?loc (str "Anonymous variables not allowed");
env
- | loc,Name id ->
+ | { loc; v = Name id } ->
check_hidden_implicit_parameters ?loc id env.impls ;
if Id.Map.is_empty ntnvars && Id.equal id ldots_var
then error_ldots_var ?loc;
set_var_scope ?loc id false (env.tmp_scope,env.scopes) ntnvars;
- if global_level then Dumpglob.dump_definition (loc,id) true "var"
+ if global_level then Dumpglob.dump_definition CAst.(make ?loc id) true "var"
else Dumpglob.dump_binding ?loc id;
{env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls}
let intern_generalized_binder ?(global_level=false) intern_type ntnvars
- env (loc, na) b b' t ty =
+ env {loc;v=na} b b' t ty =
let ids = (match na with Anonymous -> fun x -> x | Name na -> Id.Set.add na) env.ids in
let ty, ids' =
if t then ty, ids else
@@ -385,11 +387,11 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars
let ty' = intern_type {env with ids = ids; unb = true} ty in
let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty' in
let env' = List.fold_left
- (fun env (l, x) -> push_name_env ~global_level ntnvars (Variable,[],[],[])(*?*) env (l, Name x))
+ (fun env {loc;v=x} -> push_name_env ~global_level ntnvars (Variable,[],[],[])(*?*) env (make ?loc @@ Name x))
env fvs in
let bl = List.map
- (fun (loc, id) ->
- (loc, (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None))))
+ CAst.(map (fun id ->
+ (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None))))
fvs
in
let na = match na with
@@ -404,7 +406,7 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars
in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
in Name name
| _ -> na
- in (push_name_env ~global_level ntnvars (impls_type_list ty')(*?*) env' (loc,na)), (loc,(na,b',ty')) :: List.rev bl
+ in (push_name_env ~global_level ntnvars (impls_type_list ty')(*?*) env' (make ?loc na)), (make ?loc (na,b',ty')) :: List.rev bl
let intern_assumption intern ntnvars env nal bk ty =
let intern_type env = intern (set_type_scope env) in
@@ -414,9 +416,9 @@ let intern_assumption intern ntnvars env nal bk ty =
check_capture ty nal;
let impls = impls_type_list ty in
List.fold_left
- (fun (env, bl) (loc, na as locna) ->
+ (fun (env, bl) ({loc;v=na} as locna) ->
(push_name_env ntnvars impls env locna,
- (Loc.tag ?loc (na,k,locate_if_hole ?loc na ty))::bl))
+ (make ?loc (na,k,locate_if_hole ?loc na ty))::bl))
(env, []) nal
| Generalized (b,b',t) ->
let env, b = intern_generalized_binder intern_type ntnvars env (List.hd nal) b b' t ty in
@@ -434,7 +436,7 @@ let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function
let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd")
-let intern_letin_binder intern ntnvars env ((loc,na as locna),def,ty) =
+let intern_letin_binder intern ntnvars env (({loc;v=na} as locna),def,ty) =
let term = intern env def in
let ty = Option.map (intern env) ty in
(push_name_env ntnvars (impls_term_list term) env locna,
@@ -448,22 +450,22 @@ let intern_cases_pattern_as_binder ?loc ntnvars env p =
user_err ?loc (str "Unsupported nested \"as\" clause.");
il,disjpat
in
- let env = List.fold_right (fun (loc,id) env -> push_name_env ntnvars (Variable,[],[],[]) env (loc,Name id)) il env in
+ let env = List.fold_right (fun {loc;v=id} env -> push_name_env ntnvars (Variable,[],[],[]) env (make ?loc @@ Name id)) il env in
let na = alias_of_pat (List.hd disjpat) in
let ienv = Name.fold_right Id.Set.remove na env.ids in
let id = Namegen.next_name_away_with_default "pat" na ienv in
- let na = (loc, Name id) in
+ let na = make ?loc @@ Name id in
env,((disjpat,il),id),na
let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = function
| CLocalAssum(nal,bk,ty) ->
let env, bl' = intern_assumption intern ntnvars env nal bk ty in
- let bl' = List.map (fun (loc,(na,c,t)) -> DAst.make ?loc @@ GLocalAssum (na,c,t)) bl' in
+ let bl' = List.map (fun {loc;v=(na,c,t)} -> DAst.make ?loc @@ GLocalAssum (na,c,t)) bl' in
env, bl' @ bl
- | CLocalDef((loc,na as locna),def,ty) ->
+ | CLocalDef( {loc; v=na} as locna,def,ty) ->
let env,(na,bk,def,ty) = intern_letin_binder intern ntnvars env (locna,def,ty) in
env, (DAst.make ?loc @@ GLocalDef (na,bk,def,ty)) :: bl
- | CLocalPattern (loc,(p,ty)) ->
+ | CLocalPattern {loc;v=(p,ty)} ->
let tyc =
match ty with
| Some ty -> ty
@@ -472,8 +474,8 @@ let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = func
let env, ((disjpat,il),id),na = intern_cases_pattern_as_binder ?loc ntnvars env p in
let bk = Default Explicit in
let _, bl' = intern_assumption intern ntnvars env [na] bk tyc in
- let _,(_,bk,t) = List.hd bl' in
- (env, (DAst.make ?loc @@ GLocalPattern((disjpat,List.map snd il),id,bk,t)) :: bl)
+ let {v=(_,bk,t)} = List.hd bl' in
+ (env, (DAst.make ?loc @@ GLocalPattern((disjpat,List.map (fun x -> x.v) il),id,bk,t)) :: bl)
let intern_generalization intern env ntnvars loc bk ak c =
let c = intern {env with unb = true} c in
@@ -495,16 +497,16 @@ let intern_generalization intern env ntnvars loc bk ak c =
| None -> false
in
if pi then
- (fun (loc', id) acc ->
+ (fun {loc=loc';v=id} acc ->
DAst.make ?loc:(Loc.merge_opt loc' loc) @@
GProd (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
else
- (fun (loc', id) acc ->
+ (fun {loc=loc';v=id} acc ->
DAst.make ?loc:(Loc.merge_opt loc' loc) @@
GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
in
- List.fold_right (fun (loc, id as lid) (env, acc) ->
- let env' = push_name_env ntnvars (Variable,[],[],[]) env (loc, Name id) in
+ List.fold_right (fun ({loc;v=id} as lid) (env, acc) ->
+ let env' = push_name_env ntnvars (Variable,[],[],[]) env CAst.(make @@ Name id) in
(env', abs lid acc)) fvs (env,c)
in c'
@@ -571,7 +573,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
let pat, na = match disjpat with
| [pat] when is_var store pat -> let na = get () in None, na
- | _ -> Some ((List.map snd ids,disjpat),id), snd na in
+ | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in
(renaming,env), pat, na
with Not_found ->
try
@@ -581,7 +583,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
if onlyident then
(* Do not try to interpret a variable as a constructor *)
let na = out_var pat in
- let env = push_name_env ntnvars (Variable,[],[],[]) env (pat.CAst.loc, na) in
+ let env = push_name_env ntnvars (Variable,[],[],[]) env (make ?loc:pat.loc na) in
(renaming,env), None, na
else
(* Interpret as a pattern *)
@@ -589,7 +591,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
let pat, na =
match disjpat with
| [pat] when is_var store pat -> let na = get () in None, na
- | _ -> Some ((List.map snd ids,disjpat),id), snd na in
+ | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in
(renaming,env), pat, na
with Not_found ->
(* Binders not bound in the notation do not capture variables *)
@@ -601,7 +603,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
(renaming',env), None, Name id'
type binder_action =
-| AddLetIn of Name.t Loc.located * constr_expr * constr_expr option
+| AddLetIn of Misctypes.lname * constr_expr * constr_expr option
| AddTermIter of (constr_expr * subscopes) Names.Id.Map.t
| AddPreBinderIter of Id.t * local_binder_expr (* A binder to be internalized *)
| AddBinderIter of Id.t * extended_glob_local_binder (* A binder already internalized - used for generalized binders *)
@@ -692,7 +694,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
let knd = match knd with
| Evar_kinds.BinderType (Name id as na) ->
let na =
- try snd (coerce_to_name (fst (Id.Map.find id terms)))
+ try (coerce_to_name (fst (Id.Map.find id terms))).v
with Not_found ->
try Name (Id.Map.find id renaming)
with Not_found -> na
@@ -800,7 +802,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
into a substitution for interpretation and based on binding/constr
distinction *)
-let cases_pattern_of_name (loc,na) =
+let cases_pattern_of_name {loc;v=na} =
let atom = match na with Name id -> Some (Ident (loc,id)) | Anonymous -> None in
CAst.make ?loc (CPatAtom atom)
@@ -898,7 +900,7 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us =
try
let ty,expl_impls,impls,argsc = Id.Map.find id env.impls in
let expl_impls = List.map
- (fun id -> CAst.make ?loc @@ CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in
+ (fun id -> CAst.make ?loc @@ CRef (Ident (loc,id),None), Some (make ?loc @@ ExplByName id)) expl_impls in
let tys = string_of_ty ty in
Dumpglob.dump_reference ?loc "<>" (Id.to_string id) tys;
gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls
@@ -958,7 +960,7 @@ let check_no_explicitation l =
match l with
| [] -> ()
| (_, None) :: _ -> assert false
- | (_, Some (loc, _)) :: _ ->
+ | (_, Some {loc}) :: _ ->
user_err ?loc (str"Unexpected explicitation of the argument of an abbreviation.")
let dump_extended_global loc = function
@@ -1034,7 +1036,8 @@ let intern_non_secvar_qualid loc qid intern env ntnvars us args =
| GRef (VarRef _, _) -> raise Not_found
| _ -> r
-let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = function
+let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args =
+function
| Qualid (loc, qid) ->
let r,projapp,args2 =
try intern_qualid loc qid intern env ntnvars us args
@@ -1069,11 +1072,11 @@ let interp_reference vars r =
(** Private internalization patterns *)
type 'a raw_cases_pattern_expr_r =
- | RCPatAlias of 'a raw_cases_pattern_expr * Name.t Loc.located
+ | RCPatAlias of 'a raw_cases_pattern_expr * Misctypes.lname
| RCPatCstr of Globnames.global_reference
* 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list
(** [RCPatCstr (loc, c, l1, l2)] represents ((@c l1) l2) *)
- | RCPatAtom of (Id.t Loc.located * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option
+ | RCPatAtom of (Misctypes.lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option
| RCPatOr of 'a raw_cases_pattern_expr list
and 'a raw_cases_pattern_expr = ('a raw_cases_pattern_expr_r, 'a) DAst.t
@@ -1133,7 +1136,7 @@ let check_number_of_pattern loc n l =
if not (Int.equal n p) then raise (InternalizationError (loc,BadPatternsNumber (n,p)))
let check_or_pat_variables loc ids idsl =
- if List.exists (fun ids' -> not (List.eq_set (fun (loc,id) (_,id') -> Id.equal id id') ids ids')) idsl then
+ if List.exists (fun ids' -> not (List.eq_set (fun {loc;v=id} {v=id'} -> Id.equal id id') ids ids')) idsl then
user_err ?loc (str
"The components of this disjunctive pattern must bind the same variables.")
@@ -1372,7 +1375,7 @@ let sort_fields ~complete loc fields completer =
(** {6 Manage multiple aliases} *)
type alias = {
- alias_ids : Id.t Loc.located list;
+ alias_ids : Misctypes.lident list;
alias_map : Id.t Id.Map.t;
}
@@ -1383,20 +1386,20 @@ let empty_alias = {
(* [merge_aliases] returns the sets of all aliases encountered at this
point and a substitution mapping extra aliases to the first one *)
-let merge_aliases aliases (loc,na) =
+let merge_aliases aliases {loc;v=na} =
match na with
| Anonymous -> aliases
| Name id ->
- let alias_ids = aliases.alias_ids @ [loc,id] in
+ let alias_ids = aliases.alias_ids @ [make ?loc id] in
let alias_map = match aliases.alias_ids with
| [] -> aliases.alias_map
- | (_,id') :: _ -> Id.Map.add id id' aliases.alias_map
+ | {v=id'} :: _ -> Id.Map.add id id' aliases.alias_map
in
{ alias_ids; alias_map; }
let alias_of als = match als.alias_ids with
| [] -> Anonymous
-| (_,id) :: _ -> Name id
+| {v=id} :: _ -> Name id
(** {6 Expanding notations }
@@ -1426,7 +1429,7 @@ let product_of_cases_patterns aliases idspl =
let rec subst_pat_iterator y t = DAst.(map (function
| RCPatAtom id as p ->
- begin match id with Some ((_,x),_) when Id.equal x y -> DAst.get t | _ -> p end
+ begin match id with Some ({v=x},_) when Id.equal x y -> DAst.get t | _ -> p end
| RCPatCstr (id,l1,l2) ->
RCPatCstr (id,List.map (subst_pat_iterator y t) l1,
List.map (subst_pat_iterator y t) l2)
@@ -1456,7 +1459,7 @@ let drop_notations_pattern looked_for genv =
in
(** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
let rec rcp_of_glob scopes x = DAst.(map (function
- | GVar id -> RCPatAtom (Some ((x.CAst.loc,id),scopes))
+ | GVar id -> RCPatAtom (Some (CAst.make ?loc:x.loc id,scopes))
| GHole (_,_,_) -> RCPatAtom (None)
| GRef (g,_) -> RCPatCstr (g,[],[])
| GApp (r, l) ->
@@ -1562,7 +1565,7 @@ let drop_notations_pattern looked_for genv =
begin
match drop_syndef top scopes id [] with
| Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr (a, b, c)
- | None -> DAst.make ?loc @@ RCPatAtom (Some ((loc,find_pattern_variable id),scopes))
+ | None -> DAst.make ?loc @@ RCPatAtom (Some ((make ?loc @@ find_pattern_variable id),scopes))
end
| CPatAtom None -> DAst.make ?loc @@ RCPatAtom None
| CPatOr pl -> DAst.make ?loc @@ RCPatOr (List.map (in_pat top scopes) pl)
@@ -1592,7 +1595,7 @@ let drop_notations_pattern looked_for genv =
let (a,(scopt,subscopes)) = Id.Map.find id subst in
in_pat top (scopt,subscopes@snd scopes) a
with Not_found ->
- if Id.equal id ldots_var then DAst.make ?loc @@ RCPatAtom (Some ((loc,id),scopes)) else
+ if Id.equal id ldots_var then DAst.make ?loc @@ RCPatAtom (Some ((make ?loc id),scopes)) else
anomaly (str "Unbound pattern notation variable: " ++ Id.print id ++ str ".")
end
| NRef g ->
@@ -1632,7 +1635,7 @@ let rec intern_pat genv ntnvars aliases pat =
let pl' = List.map (fun (asubst,pl) ->
(asubst, DAst.make ?loc @@ PatCstr (c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in
ids',pl' in
- let loc = CAst.(pat.loc) in
+ let loc = pat.loc in
match DAst.get pat with
| RCPatAlias (p, id) ->
let aliases' = merge_aliases aliases id in
@@ -1649,8 +1652,8 @@ let rec intern_pat genv ntnvars aliases pat =
let with_letin, pl2 =
add_implicits_check_constructor_length genv loc c (List.length idslpl1 + List.length expl_pl) pl in
intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl2)
- | RCPatAtom (Some ((loc,id),scopes)) ->
- let aliases = merge_aliases aliases (loc,Name id) in
+ | RCPatAtom (Some ({loc;v=id},scopes)) ->
+ let aliases = merge_aliases aliases (make ?loc @@ Name id) in
set_var_scope ?loc id false scopes ntnvars;
(aliases.alias_ids,[aliases.alias_map, DAst.make ?loc @@ PatVar (alias_of aliases)]) (* TO CHECK: aura-t-on id? *)
| RCPatAtom (None) ->
@@ -1696,12 +1699,12 @@ let intern_ind_pattern genv ntnvars scopes pat =
let merge_impargs l args =
let test x = function
- | (_, Some (_, y)) -> explicitation_eq x y
+ | (_, Some {v=y}) -> explicitation_eq x y
| _ -> false
in
List.fold_right (fun a l ->
match a with
- | (_,Some (_,(ExplByName id as x))) when
+ | (_, Some {v=ExplByName id as x}) when
List.exists (test x) args -> l
| _ -> a::l)
l args
@@ -1733,7 +1736,7 @@ let extract_explicit_arg imps args =
let (eargs,rargs) = aux l in
match e with
| None -> (eargs,a::rargs)
- | Some (loc,pos) ->
+ | Some {loc;v=pos} ->
let id = match pos with
| ExplByName id ->
if not (exists_implicit_name id imps) then
@@ -1772,8 +1775,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
in
apply_impargs c env imp subscopes l loc
- | CFix ((locid,iddef), dl) ->
- let lf = List.map (fun ((_, id),_,_,_,_) -> id) dl in
+ | CFix ({ CAst.loc = locid; v = iddef}, dl) ->
+ let lf = List.map (fun ({CAst.v = id},_,_,_,_) -> id) dl in
let dl = Array.of_list dl in
let n =
try List.index0 Id.equal iddef lf
@@ -1808,7 +1811,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as 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 ntnvars (impls_type_list ~args:fix_args tyi)
- en (Loc.tag @@ Name name)) 0 env' lf in
+ en (CAst.make @@ Name name)) 0 env' lf in
(a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in
DAst.make ?loc @@
GRec (GFix
@@ -1817,8 +1820,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
Array.map (fun (_,bl,_,_) -> bl) idl,
Array.map (fun (_,_,ty,_) -> ty) idl,
Array.map (fun (_,_,_,bd) -> bd) idl)
- | CCoFix ((locid,iddef), dl) ->
- let lf = List.map (fun ((_, id),_,_,_) -> id) dl in
+ | CCoFix ({ CAst.loc = locid; v = iddef }, dl) ->
+ let lf = List.map (fun ({CAst.v = id},_,_,_) -> id) dl in
let dl = Array.of_list dl in
let n =
try List.index0 Id.equal iddef lf
@@ -1826,7 +1829,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
raise (InternalizationError (locid,UnboundFixName (true,iddef)))
in
let idl_tmp = Array.map
- (fun ((loc,id),bl,ty,_) ->
+ (fun ({ CAst.loc; v = id },bl,ty,_) ->
let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in
(List.rev (List.map glob_local_binder_of_extended rbl),
intern_type env' ty,env')) dl in
@@ -1835,7 +1838,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as 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 ntnvars (impls_type_list ~args:cofix_args tyi)
- en (Loc.tag @@ Name name)) 0 env' lf in
+ en (CAst.make @@ Name name)) 0 env' lf in
(b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in
DAst.make ?loc @@
GRec (GCoFix n,
@@ -1856,7 +1859,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let inc1 = intern (reset_tmp_scope env) c1 in
let int = Option.map (intern_type env) t in
DAst.make ?loc @@
- GLetIn (snd na, inc1, int,
+ GLetIn (na.CAst.v, inc1, int,
intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
| CNotation ("- _", ([a],[],[],[])) when is_non_zero a ->
let p = match a.CAst.v with CPrim (Numeral (p, _)) -> p | _ -> assert false in
@@ -1919,7 +1922,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
| CCases (sty, rtnpo, tms, eqns) ->
let as_in_vars = List.fold_left (fun acc (_,na,inb) ->
Option.fold_left (fun acc tt -> Id.Set.union (ids_of_cases_indtype tt) acc)
- (Option.fold_left (fun acc (_,y) -> Name.fold_right Id.Set.add y acc) acc na)
+ (Option.fold_left (fun acc { CAst.v = y } -> Name.fold_right Id.Set.add y acc) acc na)
inb) Id.Set.empty tms in
(* as, in & return vars *)
let forbidden_vars = Option.cata free_vars_of_constr_expr as_in_vars rtnpo in
@@ -1929,7 +1932,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
(tm,ind)::inds, Option.fold_right Id.Set.add extra_id ex_ids, List.rev_append match_td matchs)
tms ([],Id.Set.empty,[]) in
let env' = Id.Set.fold
- (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (Loc.tag @@ Name var))
+ (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (CAst.make @@ Name var))
(Id.Set.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 =
@@ -1969,17 +1972,17 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in
let p' = Option.map (fun u ->
let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
- (Loc.tag na') in
+ (CAst.make na') in
intern_type env'' u) po in
DAst.make ?loc @@
- GLetTuple (List.map snd nal, (na', p'), b',
+ GLetTuple (List.map (fun { CAst.v } -> v) nal, (na', p'), b',
intern (List.fold_left (push_name_env ntnvars (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
| CIf (c, (na,po), b1, b2) ->
let env' = reset_tmp_scope env in
let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,na,None) in (* no "in" no match to ad too *)
let p' = Option.map (fun p ->
let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env)
- (Loc.tag na') in
+ (CAst.make na') in
intern_type env'' p) po in
DAst.make ?loc @@
GIf (c', (na', p'), intern env b1, intern env b2)
@@ -2063,10 +2066,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
(ids,List.flatten mpl')
(* Expands a pattern-matching clause [lhs => rhs] *)
- and intern_eqn n env (loc,(lhs,rhs)) =
+ and intern_eqn n env {loc;v=(lhs,rhs)} =
let eqn_ids,pll = intern_disjunctive_multiple_pattern env loc n lhs in
(* Linearity implies the order in ids is irrelevant *)
- let eqn_ids = List.map snd eqn_ids in
+ let eqn_ids = List.map (fun x -> x.v) eqn_ids in
check_linearity lhs eqn_ids;
let env_ids = List.fold_right Id.Set.add eqn_ids env.ids in
List.map (fun (asubst,pl) ->
@@ -2081,10 +2084,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let extra_id,na =
let loc = tm'.CAst.loc in
match DAst.get tm', na with
- | GVar id, None when not (Id.Map.mem id (snd lvar)) -> Some id,(loc,Name id)
- | GRef (VarRef id, _), None -> Some id,(loc,Name id)
- | _, None -> None,(Loc.tag Anonymous)
- | _, Some (loc,na) -> None,(loc,na) in
+ | GVar id, None when not (Id.Map.mem id (snd lvar)) -> Some id, CAst.make ?loc @@ Name id
+ | GRef (VarRef id, _), None -> Some id, CAst.make ?loc @@ Name id
+ | _, None -> None, CAst.make Anonymous
+ | _, Some ({ CAst.loc; v = na } as lna) -> None, lna in
(* the "in" part *)
let match_td,typ = match t with
| Some t ->
@@ -2100,8 +2103,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let (match_to_do,nal) =
let rec canonize_args case_rel_ctxt arg_pats forbidden_names match_acc var_acc =
let add_name l = function
- | _,Anonymous -> l
- | loc,(Name y as x) -> (y, DAst.make ?loc @@ PatVar x) :: l in
+ | { CAst.v = Anonymous } -> l
+ | { CAst.loc; v = (Name y as x) } -> (y, DAst.make ?loc @@ PatVar x) :: l in
match case_rel_ctxt,arg_pats with
(* LetIn in the rel_context *)
| LocalDef _ :: t, l when not with_letin ->
@@ -2113,7 +2116,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
| PatVar x ->
let loc = c.CAst.loc in
canonize_args t tt forbidden_names
- (add_name match_acc (loc,x)) ((loc,x)::var_acc)
+ (add_name match_acc CAst.(make ?loc x)) ((loc,x)::var_acc)
| _ ->
let fresh =
Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names (EConstr.of_constr ty) in
@@ -2127,7 +2130,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
match_to_do, Some (cases_pattern_expr_loc t,(ind,List.rev_map snd nal))
| None ->
[], None in
- (tm',(snd na,typ)), extra_id, match_td
+ (tm',(na.CAst.v,typ)), extra_id, match_td
and intern_impargs c env l subscopes args =
let eargs, rargs = extract_explicit_arg l args in
@@ -2169,7 +2172,6 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
in aux 1 l subscopes eargs rargs
and apply_impargs c env imp subscopes l loc =
- let l : (Constrexpr.constr_expr * Constrexpr.explicitation Loc.located option) list = l in
let imp = select_impargs_size (List.length (List.filter (fun (_,x) -> x == None) l)) imp in
let l = intern_impargs c env imp subscopes l in
smart_gapp c loc l
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index f09b17a49..7411fb84b 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -87,7 +87,7 @@ val intern_gen : typing_constraint -> env ->
constr_expr -> glob_constr
val intern_pattern : env -> cases_pattern_expr ->
- Id.t Loc.located list * (Id.t Id.Map.t * cases_pattern) list
+ lident list * (Id.t Id.Map.t * cases_pattern) list
val intern_context : bool -> env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list
diff --git a/interp/declare.ml b/interp/declare.ml
index 72cdabfd2..dfa84f278 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -561,7 +561,7 @@ let do_universe poly l =
(str"Cannot declare polymorphic universes outside sections")
in
let l =
- List.map (fun (l, id) ->
+ List.map (fun {CAst.v=id} ->
let lev = Universes.new_univ_id () in
(id, lev)) l
in
diff --git a/interp/declare.mli b/interp/declare.mli
index f368d164e..9bec32d29 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -85,6 +85,6 @@ val declare_univ_binders : Globnames.global_reference -> Universes.universe_bind
val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
-val do_universe : polymorphic -> Id.t Loc.located list -> unit
+val do_universe : polymorphic -> Misctypes.lident list -> unit
val do_constraint : polymorphic -> (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list ->
unit
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index d7962e29a..e439db2b2 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -249,12 +249,12 @@ let dump_def ?loc ty secpath id = Option.iter (fun loc ->
dump_string (Printf.sprintf "%s %d:%d %s %s\n" ty bl el secpath id)
) loc
-let dump_definition (loc, id) sec s =
+let dump_definition {CAst.loc;v=id} sec s =
dump_def ?loc s (Names.DirPath.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id)
-let dump_constraint (((loc, n),_), _, _) sec ty =
+let dump_constraint (({ CAst.loc; v = n },_), _, _) sec ty =
match n with
- | Names.Name id -> dump_definition (loc, id) sec ty
+ | Names.Name id -> dump_definition CAst.(make ?loc id) sec ty
| Names.Anonymous -> ()
let dump_moddef ?loc mp ty =
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index f3ad50f28..c779e860f 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -25,7 +25,7 @@ val continue : unit -> unit
val add_glob : ?loc:Loc.t -> Globnames.global_reference -> unit
val add_glob_kn : ?loc:Loc.t -> Names.KerName.t -> unit
-val dump_definition : Names.Id.t Loc.located -> bool -> string -> unit
+val dump_definition : Misctypes.lident -> bool -> string -> unit
val dump_moddef : ?loc:Loc.t -> Names.ModPath.t -> string -> unit
val dump_modref : ?loc:Loc.t -> Names.ModPath.t -> string -> unit
val dump_reference : ?loc:Loc.t -> string -> string -> string -> unit
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index a838d7106..326969b67 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -26,7 +26,7 @@ module RelDecl = Context.Rel.Declaration
let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident"
-let declare_generalizable_ident table (loc,id) =
+let declare_generalizable_ident table {CAst.loc;v=id} =
if not (Id.equal id (root_of_id id)) then
user_err ?loc ~hdr:"declare_generalizable_ident"
((Id.print id ++ str
@@ -49,7 +49,7 @@ let cache_generalizable_type (_,(local,cmd)) =
let load_generalizable_type _ (_,(local,cmd)) =
generalizable_table := add_generalizable cmd !generalizable_table
-let in_generalizable : bool * Id.t Loc.located list option -> obj =
+let in_generalizable : bool * Misctypes.lident list option -> obj =
declare_object {(default_object "GENERALIZED-IDENT") with
load_function = load_generalizable_type;
cache_function = cache_generalizable_type;
@@ -99,7 +99,7 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
in aux bound l c
let ids_of_names l =
- List.fold_left (fun acc x -> match snd x with Name na -> na :: acc | Anonymous -> acc) [] l
+ List.fold_left (fun acc x -> match x.CAst.v with Name na -> na :: acc | Anonymous -> acc) [] l
let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr list) =
let rec aux bdvars l c = match c with
@@ -109,7 +109,7 @@ let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr li
aux (Id.Set.union (ids_of_list bound) bdvars) l' tl
| ((CLocalDef (n, c, t)) :: tl) ->
- let bound = match snd n with Anonymous -> [] | Name n -> [n] in
+ let bound = match n.CAst.v with Anonymous -> [] | Name n -> [n] in
let l' = free_vars_of_constr_expr c ~bound:bdvars l in
let l'' = Option.fold_left (fun l t -> free_vars_of_constr_expr t ~bound:bdvars l) l' t in
aux (Id.Set.union (ids_of_list bound) bdvars) l'' tl
@@ -123,13 +123,13 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp
| GVar id ->
let loc = c.CAst.loc in
if is_freevar bound (Global.env ()) id then
- if Id.List.mem_assoc_sym id vs then vs
- else (Loc.tag ?loc id) :: vs
+ if List.exists (fun {CAst.v} -> Id.equal v id) vs then vs
+ else CAst.(make ?loc id) :: vs
else vs
| _ -> Glob_ops.fold_glob_constr_with_binders Id.Set.add vars bound vs c
in fun rt ->
let vars = List.rev (vars bound [] rt) in
- List.iter (fun (loc, id) ->
+ List.iter (fun {CAst.loc;v=id} ->
if not (Id.Set.mem id allowed || find_generalizable_ident id) then
ungeneralizable loc id) vars;
vars
@@ -146,7 +146,7 @@ let combine_params avoid fn applied needed =
let named, applied =
List.partition
(function
- (t, Some (loc, ExplByName id)) ->
+ (t, Some {CAst.loc;v=ExplByName id}) ->
let is_id (_, decl) = match RelDecl.get_name decl with
| Name id' -> Id.equal id id'
| Anonymous -> false
@@ -157,7 +157,7 @@ let combine_params avoid fn applied needed =
| _ -> false) applied
in
let named = List.map
- (fun x -> match x with (t, Some (loc, ExplByName id)) -> id, t | _ -> assert false)
+ (fun x -> match x with (t, Some {CAst.loc;v=ExplByName id}) -> id, t | _ -> assert false)
named
in
let is_unset (_, decl) = match decl with
@@ -198,23 +198,23 @@ let destClassApp cl =
let open CAst in
let loc = cl.loc in
match cl.v with
- | CApp ((None, { v = CRef (ref, inst) }), l) -> Loc.tag ?loc (ref, List.map fst l, inst)
- | CAppExpl ((None, ref, inst), l) -> Loc.tag ?loc (ref, l, inst)
- | CRef (ref, inst) -> Loc.tag ?loc:(loc_of_reference ref) (ref, [], inst)
+ | CApp ((None, { v = CRef (ref, inst) }), l) -> CAst.make ?loc (ref, List.map fst l, inst)
+ | CAppExpl ((None, ref, inst), l) -> CAst.make ?loc (ref, l, inst)
+ | CRef (ref, inst) -> CAst.make ?loc:(loc_of_reference ref) (ref, [], inst)
| _ -> raise Not_found
let destClassAppExpl cl =
let open CAst in
let loc = cl.loc in
match cl.v with
- | CApp ((None, { v = CRef (ref, inst) } ), l) -> Loc.tag ?loc (ref, l, inst)
- | CRef (ref, inst) -> Loc.tag ?loc:(loc_of_reference ref) (ref, [], inst)
+ | CApp ((None, { v = CRef (ref, inst) } ), l) -> CAst.make ?loc (ref, l, inst)
+ | CRef (ref, inst) -> CAst.make ?loc:(loc_of_reference ref) (ref, [], inst)
| _ -> raise Not_found
let implicit_application env ?(allow_partial=true) f ty =
let is_class =
try
- let (_, (r, _, _) as clapp) = destClassAppExpl ty in
+ let ({CAst.v=(r, _, _)} as clapp) = destClassAppExpl ty in
let (loc, qid) = qualid_of_reference r in
let gr = Nametab.locate qid in
if Typeclasses.is_class gr then Some (clapp, gr) else None
@@ -222,7 +222,7 @@ let implicit_application env ?(allow_partial=true) f ty =
in
match is_class with
| None -> ty, env
- | Some ((loc, (id, par, inst)), gr) ->
+ | Some ({CAst.loc;v=(id, par, inst)}, gr) ->
let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
let c, avoid =
let c = class_info gr in
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index bfe73160b..625e12003 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -6,18 +6,17 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Loc
open Names
open Glob_term
open Constrexpr
open Libnames
open Globnames
-val declare_generalizable : Vernacexpr.locality_flag -> (Id.t located) list option -> unit
+val declare_generalizable : Vernacexpr.locality_flag -> Misctypes.lident list option -> unit
val ids_of_list : Id.t list -> Id.Set.t
-val destClassApp : constr_expr -> (reference * constr_expr list * instance_expr option) located
-val destClassAppExpl : constr_expr -> (reference * (constr_expr * explicitation located option) list * instance_expr option) located
+val destClassApp : constr_expr -> (reference * constr_expr list * instance_expr option) CAst.t
+val destClassAppExpl : constr_expr -> (reference * (constr_expr * explicitation CAst.t option) list * instance_expr option) CAst.t
(** Fragile, should be used only for construction a set of identifiers to avoid *)
@@ -31,7 +30,7 @@ val free_vars_of_binders :
order with the location of their first occurrence *)
val generalizable_vars_of_glob_constr : ?bound:Id.Set.t -> ?allowed:Id.Set.t ->
- glob_constr -> Id.t located list
+ glob_constr -> Misctypes.lident list
val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 04710282f..3e1a7dd9b 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -84,7 +84,7 @@ let in_reserved : Id.t * notation_constr -> obj =
declare_object {(default_object "RESERVED-TYPE") with
cache_function = cache_reserved_type }
-let declare_reserved_type_binding (loc,id) t =
+let declare_reserved_type_binding {CAst.loc;v=id} t =
if not (Id.equal id (root_of_id id)) then
user_err ?loc ~hdr:"declare_reserved_type"
((Id.print id ++ str
diff --git a/interp/reserve.mli b/interp/reserve.mli
index 4fcef23c5..5899cd628 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -6,9 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Loc
open Names
open Notation_term
-val declare_reserved_type : Id.t located list -> notation_constr -> unit
+val declare_reserved_type : Misctypes.lident list -> notation_constr -> unit
val find_reserved_type : Id.t -> notation_constr
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index ed00fe296..ea1c63b89 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -41,7 +41,7 @@ val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and
val wit_ident : Id.t uniform_genarg_type
-val wit_var : (Id.t located, Id.t located, Id.t) genarg_type
+val wit_var : (lident, lident, Id.t) genarg_type
val wit_ref : (reference, global_reference located or_var, global_reference) genarg_type
@@ -76,7 +76,7 @@ val wit_red_expr :
(glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
(constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
-val wit_clause_dft_concl : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
+val wit_clause_dft_concl : (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type
(** Aliases for compatibility *)
@@ -84,7 +84,7 @@ val wit_integer : int uniform_genarg_type
val wit_preident : string uniform_genarg_type
val wit_reference : (reference, global_reference located or_var, global_reference) genarg_type
val wit_global : (reference, global_reference located or_var, global_reference) genarg_type
-val wit_clause : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
+val wit_clause : (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type
val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
val wit_intropattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
val wit_redexpr :
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 9fc02461e..66d87707c 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Loc
open Names
open Constrexpr
@@ -15,7 +14,7 @@ val asymmetric_patterns : bool ref
[@@ocaml.deprecated "use Constrexpr_ops.asymmetric_patterns"]
(** Utilities on constr_expr *)
-val split_at_annot : local_binder_expr list -> Id.t located option -> local_binder_expr list * local_binder_expr list
+val split_at_annot : local_binder_expr list -> Misctypes.lident option -> local_binder_expr list * local_binder_expr list
[@@ocaml.deprecated "use Constrexpr_ops.split_at_annot"]
val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml
index c59828794..5b51953bb 100644
--- a/intf/constrexpr.ml
+++ b/intf/constrexpr.ml
@@ -46,7 +46,7 @@ type prim_token =
type instance_expr = Misctypes.glob_level list
type cases_pattern_expr_r =
- | CPatAlias of cases_pattern_expr * Name.t Loc.located
+ | CPatAlias of cases_pattern_expr * lname
| CPatCstr of reference
* cases_pattern_expr list option * cases_pattern_expr list
(** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *)
@@ -68,14 +68,14 @@ and cases_pattern_notation_substitution =
and constr_expr_r =
| CRef of reference * instance_expr option
- | CFix of Id.t Loc.located * fix_expr list
- | CCoFix of Id.t Loc.located * cofix_expr list
+ | CFix of lident * fix_expr list
+ | CCoFix of lident * cofix_expr list
| CProdN of local_binder_expr list * constr_expr
| CLambdaN of local_binder_expr list * constr_expr
- | CLetIn of Name.t Loc.located * constr_expr * constr_expr option * constr_expr
+ | CLetIn of lname * constr_expr * constr_expr option * constr_expr
| CAppExpl of (proj_flag * reference * instance_expr option) * constr_expr list
| CApp of (proj_flag * constr_expr) *
- (constr_expr * explicitation Loc.located option) list
+ (constr_expr * explicitation CAst.t option) list
| CRecord of (reference * constr_expr) list
(* representation of the "let" and "match" constructs *)
@@ -84,9 +84,9 @@ and constr_expr_r =
* case_expr list
* branch_expr list (* branches *)
- | CLetTuple of Name.t Loc.located list * (Name.t Loc.located option * constr_expr option) *
+ | CLetTuple of lname list * (lname option * constr_expr option) *
constr_expr * constr_expr
- | CIf of constr_expr * (Name.t Loc.located option * constr_expr option)
+ | CIf of constr_expr * (lname option * constr_expr option)
* constr_expr * constr_expr
| CHole of Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option
| CPatVar of patvar
@@ -101,18 +101,18 @@ and constr_expr_r =
and constr_expr = constr_expr_r CAst.t
and case_expr = constr_expr (* expression that is being matched *)
- * Name.t Loc.located option (* as-clause *)
+ * lname option (* as-clause *)
* cases_pattern_expr option (* in-clause *)
and branch_expr =
- (cases_pattern_expr list list * constr_expr) Loc.located
+ (cases_pattern_expr list list * constr_expr) CAst.t
and fix_expr =
- Id.t Loc.located * (Id.t Loc.located option * recursion_order_expr) *
+ lident * (lident option * recursion_order_expr) *
local_binder_expr list * constr_expr * constr_expr
and cofix_expr =
- Id.t Loc.located * local_binder_expr list * constr_expr * constr_expr
+ lident * local_binder_expr list * constr_expr * constr_expr
and recursion_order_expr =
| CStructRec
@@ -121,9 +121,9 @@ and recursion_order_expr =
(** Anonymous defs allowed ?? *)
and local_binder_expr =
- | CLocalAssum of Name.t Loc.located list * binder_kind * constr_expr
- | CLocalDef of Name.t Loc.located * constr_expr * constr_expr option
- | CLocalPattern of (cases_pattern_expr * constr_expr option) Loc.located
+ | CLocalAssum of lname list * binder_kind * constr_expr
+ | CLocalDef of lname * constr_expr * constr_expr option
+ | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t
and constr_notation_substitution =
constr_expr list * (** for constr subterms *)
diff --git a/intf/genredexpr.ml b/intf/genredexpr.ml
index a8c37c620..bdf3242ca 100644
--- a/intf/genredexpr.ml
+++ b/intf/genredexpr.ml
@@ -8,8 +8,6 @@
(** Reduction expressions *)
-open Names
-
(** The parsing produces initially a list of [red_atom] *)
type 'a red_atom =
@@ -52,7 +50,7 @@ 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 Id.t Loc.located * 'a
+ | ConstrContext of Misctypes.lident * 'a
| ConstrTypeOf of 'a
open Libnames
diff --git a/intf/misctypes.ml b/intf/misctypes.ml
index 33e961419..aafd61b3c 100644
--- a/intf/misctypes.ml
+++ b/intf/misctypes.ml
@@ -8,7 +8,13 @@
open Names
-(** Basic types used both in [constr_expr] and in [glob_constr] *)
+(** Basic types used both in [constr_expr], [glob_constr], and [vernacexpr] *)
+
+(** Located identifiers and objects with syntax. *)
+
+type lident = Id.t CAst.t
+type lname = Name.t CAst.t
+type lstring = string CAst.t
(** Cases pattern variables *)
@@ -101,9 +107,9 @@ type 'a with_bindings = 'a * 'a bindings
type 'a or_var =
| ArgArg of 'a
- | ArgVar of Names.Id.t Loc.located
+ | ArgVar of lident
-type 'a and_short_name = 'a * Id.t Loc.located option
+type 'a and_short_name = 'a * lident option
type 'a or_by_notation =
| AN of 'a
@@ -134,7 +140,7 @@ type multi =
type 'a core_destruction_arg =
| ElimOnConstr of 'a
- | ElimOnIdent of Id.t Loc.located
+ | ElimOnIdent of lident
| ElimOnAnonHyp of int
type 'a destruction_arg =
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index d16c9bb80..ba28eacea 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -6,19 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Loc
open Names
open Misctypes
open Constrexpr
-open Decl_kinds
open Libnames
(** Vernac expressions, produced by the parser *)
-
-type lident = Id.t located
-type lname = Name.t located
-type lstring = string located
-
type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation
(* spiwack: I'm choosing, for now, to have [goal_selector] be a
@@ -40,7 +33,8 @@ type goal_reference =
| NthGoal of int
| GoalId of Id.t
-type univ_name_list = Name.t Loc.located list
+type univ_name_list = Universes.univ_name_list
+[@@ocaml.deprecated "Use [Universes.univ_name_list]"]
type printable =
| PrintTables
@@ -56,7 +50,7 @@ type printable =
| PrintMLLoadPath
| PrintMLModules
| PrintDebugGC
- | PrintName of reference or_by_notation * univ_name_list option
+ | PrintName of reference or_by_notation * Universes.univ_name_list option
| PrintGraph
| PrintClasses
| PrintTypeClasses
@@ -72,7 +66,7 @@ type printable =
| PrintScopes
| PrintScope of string
| PrintVisibility of string option
- | PrintAbout of reference or_by_notation * univ_name_list option * goal_selector option
+ | PrintAbout of reference or_by_notation * Universes.univ_name_list option * goal_selector option
| PrintImplicit of reference or_by_notation
| PrintAssumptions of bool * bool * reference or_by_notation
| PrintStrategy of reference or_by_notation option
@@ -164,7 +158,7 @@ type option_ref_value =
(** Identifier and optional list of bound universes and constraints. *)
-type universe_decl_expr = (Id.t Loc.located list, glob_constraint list) gen_universe_decl
+type universe_decl_expr = (lident list, glob_constraint list) gen_universe_decl
type ident_decl = lident * universe_decl_expr option
type name_decl = lname * universe_decl_expr option
@@ -177,7 +171,7 @@ type definition_expr =
* constr_expr option
type fixpoint_expr =
- ident_decl * (Id.t located option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option
+ ident_decl * (lident option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option
type cofixpoint_expr =
ident_decl * local_binder_expr list * constr_expr * constr_expr option
@@ -205,7 +199,7 @@ type inductive_expr =
type one_inductive_expr =
ident_decl * local_binder_expr list * constr_expr option * constructor_expr list
-type typeclass_constraint = name_decl * binding_kind * constr_expr
+type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr
and typeclass_context = typeclass_constraint list
@@ -221,7 +215,7 @@ type syntax_modifier =
| SetOnlyParsing
| SetOnlyPrinting
| SetCompatVersion of Flags.compat_version
- | SetFormat of string * string located
+ | SetFormat of string * lstring
type proof_end =
| Admitted
@@ -321,7 +315,7 @@ type vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit
type vernac_argument_status = {
name : Name.t;
recarg_like : bool;
- notation_scope : string Loc.located option;
+ notation_scope : string CAst.t option;
implicit_status : vernac_implicit_status;
}
@@ -341,15 +335,15 @@ type nonrec vernac_expr =
| VernacNotationAddFormat of string * string * string
(* Gallina *)
- | VernacDefinition of (discharge * definition_object_kind) * name_decl * definition_expr
- | VernacStartTheoremProof of theorem_kind * proof_expr list
+ | VernacDefinition of (Decl_kinds.discharge * Decl_kinds.definition_object_kind) * name_decl * definition_expr
+ | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list
| VernacEndProof of proof_end
| VernacExactProof of constr_expr
- | VernacAssumption of (discharge * assumption_object_kind) *
+ | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) *
inline * (ident_decl list * constr_expr) with_coercion list
- | VernacInductive of cumulative_inductive_parsing_flag * private_flag * inductive_flag * (inductive_expr * decl_notation list) list
- | VernacFixpoint of discharge * (fixpoint_expr * decl_notation list) list
- | VernacCoFixpoint of discharge * (cofixpoint_expr * decl_notation list) list
+ | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
+ | VernacFixpoint of Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list
+ | VernacCoFixpoint of Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list
| VernacScheme of (lident option * scheme) list
| VernacCombinedScheme of lident * lident list
| VernacUniverse of lident list
@@ -416,7 +410,7 @@ type nonrec vernac_expr =
| VernacCreateHintDb of string * bool
| VernacRemoveHints of string list * reference list
| VernacHints of string list * hints_expr
- | VernacSyntacticDefinition of Id.t located * (Id.t list * constr_expr) *
+ | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) *
onlyparsing_flag
| VernacDeclareImplicits of reference or_by_notation *
(explicitation * bool * bool) list list
@@ -482,8 +476,8 @@ type vernac_control =
| VernacExpr of vernac_flag list * vernac_expr
(* boolean is true when the `-time` batch-mode command line flag was set.
the flag is used to print differently in `-time` vs `Time foo` *)
- | VernacTime of bool * vernac_control located
- | VernacRedirect of string * vernac_control located
+ | VernacTime of bool * vernac_control CAst.t
+ | VernacRedirect of string * vernac_control CAst.t
| VernacTimeout of int * vernac_control
| VernacFail of vernac_control
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 28a04252a..291039d19 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -451,7 +451,7 @@ let intern_arg interp_modast (acc, cst) (idl,(typ,ann)) =
let env = Global.env () in
let sobjs = get_module_sobjs false env inl mty in
let mp0 = get_module_path mty in
- let fold acc (_, id) =
+ let fold acc {CAst.v=id} =
let dir = DirPath.make [id] in
let mbid = MBId.make lib_dir id in
let mp = MPbound mbid in
@@ -982,8 +982,7 @@ type 'modast module_interpretor =
Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t
type 'modast module_params =
- (Id.t Loc.located list * ('modast * inline)) list
-
+ (lident list * ('modast * inline)) list
(** {6 Debug} *)
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 0df55f34d..db2893376 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -16,7 +16,7 @@ type 'modast module_interpretor =
Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t
type 'modast module_params =
- (Id.t Loc.located list * ('modast * inline)) list
+ (Misctypes.lident list * ('modast * inline)) list
(** [declare_module interp_modast id fargs typ exprs]
declares module [id], with structure constructed by [interp_modast]
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index a3d257154..cad837d08 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -226,7 +226,7 @@ type _ target =
type prod_info = production_level * production_position
type (_, _) entry =
-| TTName : ('self, Name.t Loc.located) entry
+| TTName : ('self, Misctypes.lname) entry
| TTReference : ('self, reference) entry
| TTBigint : ('self, Constrexpr.raw_natural_number) entry
| TTConstr : prod_info * 'r target -> ('r, 'r) entry
@@ -308,7 +308,7 @@ let interp_entry forpat e = match e with
| ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList
| ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl)
-let cases_pattern_expr_of_name (loc,na) = CAst.make ?loc @@ match na with
+let cases_pattern_expr_of_name { CAst.loc; v = na } = CAst.make ?loc @@ match na with
| Anonymous -> CPatAtom None
| Name id -> CPatAtom (Some (Ident (Loc.tag ?loc id)))
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 9f12db649..8a1e6d121 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -36,21 +36,21 @@ let mk_cast = function
let loc = Loc.merge_opt (constr_loc c) (constr_loc ty)
in CAst.make ?loc @@ CCast(c, CastConv ty)
-let binder_of_name expl (loc,na) =
- CLocalAssum ([loc, na], Default expl,
+let binder_of_name expl { CAst.loc = loc; v = na } =
+ CLocalAssum ([CAst.make ?loc na], Default expl,
CAst.make ?loc @@ CHole (Some (Evar_kinds.BinderType na), IntroAnonymous, None))
let binders_of_names l =
List.map (binder_of_name Explicit) l
-let mk_fixb (id,bl,ann,body,(loc,tyc)) =
+let mk_fixb (id,bl,ann,body,(loc,tyc)) : fix_expr =
let ty = match tyc with
Some ty -> ty
| None -> CAst.make @@ CHole (None, IntroAnonymous, None) in
(id,ann,bl,ty,body)
-let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
- let _ = Option.map (fun (aloc,_) ->
+let mk_cofixb (id,bl,ann,body,(loc,tyc)) : cofix_expr =
+ let _ = Option.map (fun { CAst.loc = aloc } ->
CErrors.user_err ?loc:aloc
~hdr:"Constr:mk_cofixb"
(Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in
@@ -61,10 +61,10 @@ let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
let mk_fix(loc,kw,id,dcls) =
if kw then
- let fb = List.map mk_fixb dcls in
+ let fb : fix_expr list = List.map mk_fixb dcls in
CAst.make ~loc @@ CFix(id,fb)
else
- let fb = List.map mk_cofixb dcls in
+ let fb : cofix_expr list = List.map mk_cofixb dcls in
CAst.make ~loc @@ CCoFix(id,fb)
let mk_single_fix (loc,kw,dcl) =
@@ -131,7 +131,7 @@ GEXTEND Gram
[ [ id = Prim.ident -> id ] ]
;
Prim.name:
- [ [ "_" -> Loc.tag ~loc:!@loc Anonymous ] ]
+ [ [ "_" -> CAst.make ~loc:!@loc Anonymous ] ]
;
global:
[ [ r = Prim.reference -> r ] ]
@@ -196,8 +196,9 @@ GEXTEND Gram
| "10" LEFTA
[ f=operconstr; args=LIST1 appl_arg -> CAst.make ~loc:(!@loc) @@ CApp((None,f),args)
| "@"; f=global; i = instance; args=LIST0 NEXT -> CAst.make ~loc:!@loc @@ CAppExpl((None,f,i),args)
- | "@"; (locid,id) = pattern_identref; args=LIST1 identref ->
- let args = List.map (fun x -> CAst.make @@ CRef (Ident x,None), None) args in
+ | "@"; lid = pattern_identref; args=LIST1 identref ->
+ let { CAst.loc = locid; v = id } = lid in
+ let args = List.map (fun x -> CAst.make @@ CRef (Ident Loc.(tag ?loc:x.CAst.loc x.CAst.v), None), None) args in
CAst.make ~loc:(!@loc) @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) ]
| "9"
[ ".."; c = operconstr LEVEL "0"; ".." ->
@@ -256,11 +257,11 @@ GEXTEND Gram
Option.map (mkCProdN ?loc:(fst ty) bl) (snd ty), c2)
| "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" ->
let fixp = mk_single_fix fx in
- let (li,id) = match fixp.CAst.v with
+ let { CAst.loc = li; v = id } = match fixp.CAst.v with
CFix(id,_) -> id
| CCoFix(id,_) -> id
| _ -> assert false in
- CAst.make ~loc:!@loc @@ CLetIn((li,Name id),fixp,None,c)
+ CAst.make ~loc:!@loc @@ CLetIn( CAst.make ?loc:li @@ Name id,fixp,None,c)
| "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> l | "()" -> []];
po = return_type;
":="; c1 = operconstr LEVEL "200"; "in";
@@ -269,17 +270,17 @@ GEXTEND Gram
| "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
"in"; c2 = operconstr LEVEL "200" ->
CAst.make ~loc:!@loc @@
- CCases (LetPatternStyle, None, [c1, None, None], [Loc.tag ~loc:!@loc ([[p]], c2)])
+ CCases (LetPatternStyle, None, [c1, None, None], [CAst.make ~loc:!@loc ([[p]], c2)])
| "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
rt = case_type; "in"; c2 = operconstr LEVEL "200" ->
CAst.make ~loc:!@loc @@
- CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [Loc.tag ~loc:!@loc ([[p]], c2)])
+ CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [CAst.make ~loc:!@loc ([[p]], c2)])
| "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200";
":="; c1 = operconstr LEVEL "200"; rt = case_type;
"in"; c2 = operconstr LEVEL "200" ->
CAst.make ~loc:!@loc @@
- CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [Loc.tag ~loc:!@loc ([[p]], c2)])
+ CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [CAst.make ~loc:!@loc ([[p]], c2)])
| "if"; c=operconstr LEVEL "200"; po = return_type;
"then"; b1=operconstr LEVEL "200";
"else"; b2=operconstr LEVEL "200" ->
@@ -288,7 +289,7 @@ GEXTEND Gram
;
appl_arg:
[ [ id = lpar_id_coloneq; c=lconstr; ")" ->
- (c,Some (Loc.tag ~loc:!@loc @@ ExplByName id))
+ (c,Some (CAst.make ~loc:!@loc @@ ExplByName id))
| c=operconstr LEVEL "9" -> (c,None) ] ]
;
atomic_constr:
@@ -368,7 +369,7 @@ GEXTEND Gram
;
eqn:
[ [ pll = LIST1 mult_pattern SEP "|";
- "=>"; rhs = lconstr -> (Loc.tag ~loc:!@loc (pll,rhs)) ] ]
+ "=>"; rhs = lconstr -> (CAst.make ~loc:!@loc (pll,rhs)) ] ]
;
record_pattern:
[ [ id = global; ":="; pat = pattern -> (id, pat) ] ]
@@ -420,7 +421,8 @@ GEXTEND Gram
(fun na -> CLocalAssum (na::nal,Default Implicit,c))
| nal=LIST1 name; "}" ->
(fun na -> CLocalAssum (na::nal,Default Implicit,
- CAst.make ?loc:(Loc.merge_opt (fst na) (Some !@loc)) @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None)))
+ CAst.make ?loc:(Loc.merge_opt na.CAst.loc (Some !@loc)) @@
+ CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None)))
| ":"; c=lconstr; "}" ->
(fun na -> CLocalAssum ([na],Default Implicit,c))
] ]
@@ -433,7 +435,7 @@ GEXTEND Gram
] ]
;
impl_name_head:
- [ [ id = impl_ident_head -> (Loc.tag ~loc:!@loc @@ Name id) ] ]
+ [ [ id = impl_ident_head -> (CAst.make ~loc:!@loc @@ Name id) ] ]
;
binders_fixannot:
[ [ na = impl_name_head; assum = impl_ident_tail; bl = binders_fixannot ->
@@ -453,7 +455,7 @@ GEXTEND Gram
| id = name; idl = LIST0 name; bl = binders ->
binders_of_names (id::idl) @ bl
| id1 = name; ".."; id2 = name ->
- [CLocalAssum ([id1;(Loc.tag ~loc:!@loc (Name ldots_var));id2],
+ [CLocalAssum ([id1;(CAst.make ~loc:!@loc (Name ldots_var));id2],
Default Explicit, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))]
| bl = closed_binder; bl' = binders ->
bl@bl'
@@ -495,17 +497,17 @@ GEXTEND Gram
| CPatCast (p, ty) -> (p, Some ty)
| _ -> (p, None)
in
- [CLocalPattern (Loc.tag ~loc:!@loc (p, ty))]
+ [CLocalPattern (CAst.make ~loc:!@loc (p, ty))]
] ]
;
typeclass_constraint:
- [ [ "!" ; c = operconstr LEVEL "200" -> (Loc.tag ~loc:!@loc Anonymous), true, c
+ [ [ "!" ; c = operconstr LEVEL "200" -> (CAst.make ~loc:!@loc Anonymous), true, c
| "{"; id = name; "}"; ":" ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" ->
id, expl, c
| iid=name_colon ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" ->
- (Loc.tag ~loc:!@loc iid), expl, c
+ (CAst.make ~loc:!@loc iid), expl, c
| c = operconstr LEVEL "200" ->
- (Loc.tag ~loc:!@loc Anonymous), false, c
+ (CAst.make ~loc:!@loc Anonymous), false, c
] ]
;
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 891c232ee..0b7efe739 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -43,13 +43,13 @@ GEXTEND Gram
[ [ LEFTQMARK; id = ident -> id ] ]
;
pattern_identref:
- [ [ id = pattern_ident -> Loc.tag ~loc:!@loc id ] ]
+ [ [ id = pattern_ident -> CAst.make ~loc:!@loc id ] ]
;
var: (* as identref, but interpret as a term identifier in ltac *)
- [ [ id = ident -> Loc.tag ~loc:!@loc id ] ]
+ [ [ id = ident -> CAst.make ~loc:!@loc id ] ]
;
identref:
- [ [ id = ident -> Loc.tag ~loc:!@loc id ] ]
+ [ [ id = ident -> CAst.make ~loc:!@loc id ] ]
;
field:
[ [ s = FIELD -> Id.of_string s ] ]
@@ -70,8 +70,8 @@ GEXTEND Gram
] ]
;
name:
- [ [ IDENT "_" -> Loc.tag ~loc:!@loc Anonymous
- | id = ident -> Loc.tag ~loc:!@loc @@ Name id ] ]
+ [ [ IDENT "_" -> CAst.make ~loc:!@loc Anonymous
+ | id = ident -> CAst.make ~loc:!@loc @@ Name id ] ]
;
reference:
[ [ id = ident; (l,id') = fields ->
@@ -95,7 +95,7 @@ GEXTEND Gram
] ]
;
ne_lstring:
- [ [ s = ne_string -> Loc.tag ~loc:!@loc s ] ]
+ [ [ s = ne_string -> CAst.make ~loc:!@loc s ] ]
;
dirpath:
[ [ id = ident; l = LIST0 field ->
@@ -105,7 +105,7 @@ GEXTEND Gram
[ [ s = STRING -> s ] ]
;
lstring:
- [ [ s = string -> (Loc.tag ~loc:!@loc s) ] ]
+ [ [ s = string -> (CAst.make ~loc:!@loc s) ] ]
;
integer:
[ [ i = INT -> my_int_of_string (!@loc) i
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 1c3ba7837..482373150 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -29,7 +29,7 @@ GEXTEND Gram
;
command:
[ [ IDENT "Goal"; c = lconstr ->
- VernacDefinition (Decl_kinds.(NoDischarge, Definition), ((Loc.tag ~loc:!@loc Names.Anonymous), None), ProveBody ([], c))
+ VernacDefinition (Decl_kinds.(NoDischarge, Definition), ((CAst.make ~loc:!@loc Names.Anonymous), None), ProveBody ([], c))
| IDENT "Proof" -> VernacProof (None,None)
| IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn
| IDENT "Proof"; c = lconstr -> VernacExactProof c
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index d90fd3eb7..93e534e0b 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -115,7 +115,7 @@ GEXTEND Gram
;
located_vernac:
- [ [ v = vernac_control -> Loc.tag ~loc:!@loc v ] ]
+ [ [ v = vernac_control -> CAst.make ~loc:!@loc v ] ]
;
END
@@ -134,7 +134,7 @@ let test_plural_form_types loc kwd = function
| _ -> ()
let lname_of_lident : lident -> lname =
- Loc.map (fun s -> Name s)
+ CAst.map (fun s -> Name s)
let name_of_ident_decl : ident_decl -> name_decl =
on_fst lname_of_lident
@@ -629,12 +629,12 @@ GEXTEND Gram
VernacCanonical (ByNotation ntn)
| IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body ->
let s = coerce_reference_to_id qid in
- VernacDefinition ((NoDischarge,CanonicalStructure),((Loc.tag (Name s)),None),d)
+ VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make (Name s)),None),d)
(* Coercions *)
| IDENT "Coercion"; qid = global; d = def_body ->
let s = coerce_reference_to_id qid in
- VernacDefinition ((NoDischarge,Coercion),((Loc.tag (Name s)),None),d)
+ VernacDefinition ((NoDischarge,Coercion),((CAst.make (Name s)),None),d)
| IDENT "Identity"; IDENT "Coercion"; f = identref; ":";
s = class_rawexpr; ">->"; t = class_rawexpr ->
VernacIdentityCoercion (f, s, t)
@@ -745,7 +745,7 @@ GEXTEND Gram
;
argument_spec: [
[ b = OPT "!"; id = name ; s = OPT scope ->
- snd id, not (Option.is_empty b), Option.map (fun x -> Loc.tag ~loc:!@loc x) s
+ id.CAst.v, not (Option.is_empty b), Option.map (fun x -> CAst.make ~loc:!@loc x) s
]
];
(* List of arguments implicit status, scope, modifiers *)
@@ -758,7 +758,7 @@ GEXTEND Gram
| "/" -> [`Slash]
| "("; items = LIST1 argument_spec; ")"; sc = OPT scope ->
let f x = match sc, x with
- | None, x -> x | x, None -> Option.map (fun y -> Loc.tag ~loc:!@loc y) x
+ | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc:!@loc y) x
| Some _, Some _ -> user_err Pp.(str "scope declared twice") in
List.map (fun (name,recarg_like,notation_scope) ->
`Id { name=name; recarg_like=recarg_like;
@@ -766,7 +766,7 @@ GEXTEND Gram
implicit_status = NotImplicit}) items
| "["; items = LIST1 argument_spec; "]"; sc = OPT scope ->
let f x = match sc, x with
- | None, x -> x | x, None -> Option.map (fun y -> Loc.tag ~loc:!@loc y) x
+ | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc:!@loc y) x
| Some _, Some _ -> user_err Pp.(str "scope declared twice") in
List.map (fun (name,recarg_like,notation_scope) ->
`Id { name=name; recarg_like=recarg_like;
@@ -774,7 +774,7 @@ GEXTEND Gram
implicit_status = Implicit}) items
| "{"; items = LIST1 argument_spec; "}"; sc = OPT scope ->
let f x = match sc, x with
- | None, x -> x | x, None -> Option.map (fun y -> Loc.tag ~loc:!@loc y) x
+ | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc:!@loc y) x
| Some _, Some _ -> user_err Pp.(str "scope declared twice") in
List.map (fun (name,recarg_like,notation_scope) ->
`Id { name=name; recarg_like=recarg_like;
@@ -784,11 +784,11 @@ GEXTEND Gram
];
(* Same as [argument_spec_block], but with only implicit status and names *)
more_implicits_block: [
- [ name = name -> [(snd name, Vernacexpr.NotImplicit)]
+ [ name = name -> [(name.CAst.v, Vernacexpr.NotImplicit)]
| "["; items = LIST1 name; "]" ->
- List.map (fun name -> (snd name, Vernacexpr.Implicit)) items
+ List.map (fun name -> (name.CAst.v, Vernacexpr.Implicit)) items
| "{"; items = LIST1 name; "}" ->
- List.map (fun name -> (snd name, Vernacexpr.MaximallyImplicit)) items
+ List.map (fun name -> (name.CAst.v, Vernacexpr.MaximallyImplicit)) items
]
];
strategy_level:
@@ -800,9 +800,9 @@ GEXTEND Gram
;
instance_name:
[ [ name = ident_decl; sup = OPT binders ->
- (let ((loc,id),l) = name in ((loc, Name id),l)),
+ (CAst.map (fun id -> Name id) (fst name), snd name),
(Option.default [] sup)
- | -> ((Loc.tag ~loc:!@loc Anonymous), None), [] ] ]
+ | -> ((CAst.make ~loc:!@loc Anonymous), None), [] ] ]
;
hint_info:
[ [ "|"; i = OPT natural; pat = OPT constr_pattern ->
@@ -1134,8 +1134,8 @@ GEXTEND Gram
| IDENT "Reserved"; IDENT "Infix"; s = ne_lstring;
l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] ->
- let (loc,s) = s in
- VernacSyntaxExtension (true,((loc,"x '"^s^"' y"),l))
+ let s = CAst.map (fun s -> "x '"^s^"' y") s in
+ VernacSyntaxExtension (true,(s,l))
| IDENT "Reserved"; IDENT "Notation";
s = ne_lstring;
@@ -1166,10 +1166,10 @@ GEXTEND Gram
| IDENT "only"; IDENT "parsing" -> SetOnlyParsing
| IDENT "compat"; s = STRING ->
SetCompatVersion (parse_compat_version s)
- | IDENT "format"; s1 = [s = STRING -> Loc.tag ~loc:!@loc s];
- s2 = OPT [s = STRING -> Loc.tag ~loc:!@loc s] ->
+ | IDENT "format"; s1 = [s = STRING -> CAst.make ~loc:!@loc s];
+ s2 = OPT [s = STRING -> CAst.make ~loc:!@loc s] ->
begin match s1, s2 with
- | (_,k), Some s -> SetFormat(k,s)
+ | { CAst.v = k }, Some s -> SetFormat(k,s)
| s, None -> SetFormat ("text",s) end
| x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at";
lev = level -> SetItemLevel (x::l,lev)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index accb51366..f36250176 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -192,17 +192,17 @@ module Prim :
open Libnames
val preident : string Gram.entry
val ident : Id.t Gram.entry
- val name : Name.t located Gram.entry
- val identref : Id.t located Gram.entry
+ val name : lname Gram.entry
+ val identref : lident Gram.entry
val ident_decl : ident_decl Gram.entry
val pattern_ident : Id.t Gram.entry
- val pattern_identref : Id.t located Gram.entry
+ val pattern_identref : lident Gram.entry
val base_ident : Id.t Gram.entry
val natural : int Gram.entry
val bigint : Constrexpr.raw_natural_number Gram.entry
val integer : int Gram.entry
val string : string Gram.entry
- val lstring : string located Gram.entry
+ val lstring : lstring Gram.entry
val qualid : qualid located Gram.entry
val fullyqualid : Id.t list located Gram.entry
val reference : reference Gram.entry
@@ -210,8 +210,8 @@ module Prim :
val smart_global : reference or_by_notation Gram.entry
val dirpath : DirPath.t Gram.entry
val ne_string : string Gram.entry
- val ne_lstring : string located Gram.entry
- val var : Id.t located Gram.entry
+ val ne_lstring : lstring Gram.entry
+ val var : lident Gram.entry
end
module Constr :
@@ -233,10 +233,10 @@ module Constr :
val binder : local_binder_expr list Gram.entry (* closed_binder or variable *)
val binders : local_binder_expr list Gram.entry (* list of binder *)
val open_binders : local_binder_expr list Gram.entry
- val binders_fixannot : (local_binder_expr list * (Id.t located option * recursion_order_expr)) Gram.entry
- val typeclass_constraint : (Name.t located * bool * constr_expr) Gram.entry
+ val binders_fixannot : (local_binder_expr list * (lident option * recursion_order_expr)) Gram.entry
+ val typeclass_constraint : (lname * bool * constr_expr) Gram.entry
val record_declaration : constr_expr Gram.entry
- val appl_arg : (constr_expr * explicitation located option) Gram.entry
+ val appl_arg : (constr_expr * explicitation CAst.t option) Gram.entry
end
module Module :
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)
diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml
index 3cf32d7ff..89f1185a9 100644
--- a/pretyping/univdecls.ml
+++ b/pretyping/univdecls.ml
@@ -6,12 +6,11 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Names
open CErrors
(** Local universes and constraints declarations *)
type universe_decl =
- (Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+ (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
let default_univ_decl =
let open Misctypes in
@@ -34,9 +33,9 @@ let interp_univ_constraints env evd cstrs =
in
List.fold_left interp (evd,Univ.Constraint.empty) cstrs
-let interp_univ_decl env decl =
+let interp_univ_decl env decl =
let open Misctypes in
- let pl = decl.univdecl_instance in
+ let pl : lident list = decl.univdecl_instance in
let evd = Evd.from_ctx (Evd.make_evar_universe_context env (Some pl)) in
let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
let decl = { univdecl_instance = pl;
diff --git a/pretyping/univdecls.mli b/pretyping/univdecls.mli
index 0c3b749cb..706d3a157 100644
--- a/pretyping/univdecls.mli
+++ b/pretyping/univdecls.mli
@@ -8,7 +8,7 @@
(** Local universe and constraint declarations. *)
type universe_decl =
- (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+ (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
val default_univ_decl : universe_decl
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 873505940..3c7095505 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -10,6 +10,7 @@
open CErrors
open Util
open Pp
+open CAst
open Names
open Nameops
open Libnames
@@ -151,7 +152,7 @@ let tag_var = tag Tag.variable
if !Flags.beautify && not (Int.equal n 0) then comment (CLexer.extract_comments n)
else mt()
- let pr_with_comments ?loc pp = pr_located (fun x -> x) (Loc.tag ?loc pp)
+ let pr_with_comments ?loc pp = pr_located (fun x -> x) (loc, pp)
let pr_sep_com sep f c = pr_with_comments ?loc:(constr_loc c) (sep() ++ f c)
@@ -220,28 +221,28 @@ let tag_var = tag Tag.variable
let pr_expl_args pr (a,expl) =
match expl with
| None -> pr (lapp,L) a
- | Some (_,ExplByPos (n,_id)) ->
+ | Some {v=ExplByPos (n,_id)} ->
anomaly (Pp.str "Explicitation by position not implemented.")
- | Some (_,ExplByName id) ->
+ | Some {v=ExplByName id} ->
str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")"
let pr_opt_type_spc pr = function
| { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> mt ()
| t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
- let pr_lident (loc,id) =
+ let pr_lident {loc; v=id} =
match loc with
| None -> pr_id id
| Some loc -> let (b,_) = Loc.unloc loc in
- pr_located pr_id @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (Id.to_string id))) id
+ pr_located pr_id (Some (Loc.make_loc (b,b + String.length (Id.to_string id))), id)
let pr_lname = function
- | (loc,Name id) -> pr_lident (loc,id)
- | lna -> pr_located Name.print lna
+ | {CAst.loc; v=Name id} -> pr_lident CAst.(make ?loc id)
+ | x -> pr_ast Name.print x
let pr_or_var pr = function
| ArgArg x -> pr x
- | ArgVar (loc,s) -> pr_lident (loc,s)
+ | ArgVar id -> pr_lident id
let pr_prim_token = function
| Numeral (n,s) -> str (if s then n else "-"^n)
@@ -315,7 +316,7 @@ let tag_var = tag Tag.variable
let pr_patt = pr_patt mt
- let pr_eqn pr (loc,(pl,rhs)) =
+ let pr_eqn pr {loc;v=(pl,rhs)} =
spc() ++ hov 4
(pr_with_comments ?loc
(str "| " ++
@@ -323,12 +324,12 @@ let tag_var = tag Tag.variable
++ str " =>") ++
pr_sep_com spc (pr ltop) rhs))
- let begin_of_binder l_bi =
+ let begin_of_binder l_bi =
let b_loc l = fst (Option.cata Loc.unloc (0,0) l) in
match l_bi with
- | CLocalDef((loc,_),_,_) -> b_loc loc
- | CLocalAssum((loc,_)::_,_,_) -> b_loc loc
- | CLocalPattern(loc,(_,_)) -> b_loc loc
+ | CLocalDef({loc},_,_) -> b_loc loc
+ | CLocalAssum({loc}::_,_,_) -> b_loc loc
+ | CLocalPattern{loc} -> b_loc loc
| _ -> assert false
let begin_of_binders = function
@@ -350,12 +351,12 @@ let tag_var = tag Tag.variable
| Generalized (b, b', t') ->
assert (match b with Implicit -> true | _ -> false);
begin match nal with
- |[loc,Anonymous] ->
+ |[{loc; v=Anonymous}] ->
hov 1 (str"`" ++ (surround_impl b'
((if t' then str "!" else mt ()) ++ pr t)))
- |[loc,Name id] ->
+ |[{loc; v=Name id}] ->
hov 1 (str "`" ++ (surround_impl b'
- (pr_lident (loc,id) ++ str " : " ++
+ (pr_lident CAst.(make ?loc id) ++ str " : " ++
(if t' then str "!" else mt()) ++ pr t)))
|_ -> anomaly (Pp.str "List of generalized binders have alwais one element.")
end
@@ -375,7 +376,7 @@ let tag_var = tag Tag.variable
surround (pr_lname na ++
pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr_c t) topt ++
str" :=" ++ spc() ++ pr_c c)
- | CLocalPattern (loc,(p,tyo)) ->
+ | CLocalPattern {CAst.loc; v = p,tyo} ->
let p = pr_patt lsimplepatt p in
match tyo with
| None ->
@@ -410,7 +411,7 @@ let tag_var = tag Tag.variable
let pr_guard_annot pr_aux bl (n,ro) =
match n with
| None -> mt ()
- | Some (loc, id) ->
+ | Some {loc; v = id} ->
match (ro : Constrexpr.recursion_order_expr) with
| CStructRec ->
let names_of_binder = function
@@ -427,11 +428,11 @@ let tag_var = tag Tag.variable
spc() ++ str "{" ++ keyword "measure" ++ spc () ++ pr_aux m ++ spc() ++ pr_id id++
(match r with None -> mt() | Some r -> str" on " ++ pr_aux r) ++ str"}"
- let pr_fixdecl pr prd dangling_with_for ((_,id),ro,bl,t,c) =
+ let pr_fixdecl pr prd dangling_with_for ({v=id},ro,bl,t,c) =
let annot = pr_guard_annot (pr lsimpleconstr) bl ro in
pr_recursive_decl pr prd dangling_with_for id bl annot t c
- let pr_cofixdecl pr prd dangling_with_for ((_,id),bl,t,c) =
+ let pr_cofixdecl pr prd dangling_with_for ({v=id},bl,t,c) =
pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c
let pr_recursive pr_decl id = function
@@ -461,7 +462,7 @@ let tag_var = tag Tag.variable
let pr_simple_return_type pr na po =
(match na with
- | Some (_,Name id) ->
+ | Some {v=Name id} ->
spc () ++ keyword "as" ++ spc () ++ pr_id id
| _ -> mt ()) ++
pr_case_type pr po
@@ -492,7 +493,7 @@ let tag_var = tag Tag.variable
let pr_fun_sep = spc () ++ str "=>"
let pr_dangling_with_for sep pr inherited a =
- match a.CAst.v with
+ match a.v with
| (CFix (_,[_])|CCoFix(_,[_])) ->
pr sep (latom,E) a
| _ ->
@@ -507,14 +508,14 @@ let tag_var = tag Tag.variable
return (
hov 0 (keyword "fix" ++ spc () ++
pr_recursive
- (pr_fixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) fix),
+ (pr_fixdecl (pr mt) (pr_dangling_with_for mt pr)) id.v fix),
lfix
)
| CCoFix (id,cofix) ->
return (
hov 0 (keyword "cofix" ++ spc () ++
pr_recursive
- (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) cofix),
+ (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) id.v cofix),
lfix
)
| CProdN (bl,a) ->
@@ -533,8 +534,8 @@ let tag_var = tag Tag.variable
pr_fun_sep ++ pr spc ltop a),
llambda
)
- | CLetIn ((_,Name x), ({ CAst.v = CFix((_,x'),[_])}
- | { CAst.v = CCoFix((_,x'),[_]) } as fx), t, b)
+ | CLetIn ({v=Name x}, ({ v = CFix({v=x'},[_])}
+ | { v = CCoFix({v=x'},[_]) } as fx), t, b)
when Id.equal x x' ->
return (
hv 0 (
@@ -590,7 +591,7 @@ let tag_var = tag Tag.variable
hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"),
latom
)
- | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,([[p]],b))]) ->
+ | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) ->
return (
hv 0 (
keyword "let" ++ spc () ++ str"'" ++
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 158906dd2..cedeed5f3 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -10,7 +10,6 @@
objects and their subcomponents. *)
(** The default pretty-printers produce pretty-printing commands ({!Pp.t}). *)
-open Loc
open Libnames
open Constrexpr
open Names
@@ -23,8 +22,8 @@ val pr_tight_coma : unit -> Pp.t
val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t
-val pr_lident : Id.t located -> Pp.t
-val pr_lname : Name.t located -> Pp.t
+val pr_lident : lident -> Pp.t
+val pr_lname : lname -> Pp.t
val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t
val pr_com_at : int -> Pp.t
@@ -44,7 +43,7 @@ val pr_glob_level : glob_level -> Pp.t
val pr_glob_sort : glob_sort -> Pp.t
val pr_guard_annot : (constr_expr -> Pp.t) ->
local_binder_expr list ->
- ('a * Names.Id.t) option * recursion_order_expr ->
+ lident option * recursion_order_expr ->
Pp.t
val pr_record_body : (reference * constr_expr) list -> Pp.t
diff --git a/printing/pputils.ml b/printing/pputils.ml
index a544b4762..e779fc5fc 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -24,9 +24,11 @@ let pr_located pr (loc, x) =
before ++ x ++ after
| _ -> pr x
+let pr_ast pr { CAst.loc; v } = pr_located pr (loc, v)
+
let pr_or_var pr = function
| ArgArg x -> pr x
- | ArgVar (_,s) -> Names.Id.print s
+ | ArgVar {CAst.v=s} -> Names.Id.print s
let pr_with_occurrences pr keyword (occs,c) =
match occs with
diff --git a/printing/pputils.mli b/printing/pputils.mli
index f7f586b77..ec5c32fc4 100644
--- a/printing/pputils.mli
+++ b/printing/pputils.mli
@@ -12,6 +12,7 @@ open Locus
open Genredexpr
val pr_located : ('a -> Pp.t) -> 'a Loc.located -> Pp.t
+val pr_ast : ('a -> Pp.t) -> 'a CAst.t -> Pp.t
(** Prints an object surrounded by its commented location *)
val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 31c0d20f3..83cac7ddd 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -11,6 +11,8 @@ open Names
open CErrors
open Util
+open CAst
+
open Extend
open Vernacexpr
open Pputils
@@ -59,7 +61,7 @@ open Decl_kinds
let pr_ident_decl (lid, l) =
pr_lident lid ++ pr_universe_decl l
-
+
let string_of_fqid fqid =
String.concat "." (List.map Id.to_string fqid)
@@ -236,7 +238,7 @@ open Decl_kinds
keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++
pr_located pr_qualid qid
- let rec pr_module_ast leading_space pr_c = let open CAst in function
+ let rec pr_module_ast leading_space pr_c = function
| { loc ; v = CMident qid } ->
if leading_space then
spc () ++ pr_located pr_qualid (loc, qid)
@@ -287,10 +289,10 @@ open Decl_kinds
prlist_strict (pr_module_vardecls pr_c) l
let pr_type_option pr_c = function
- | { CAst.v = CHole (k, Misctypes.IntroAnonymous, _) } -> mt()
+ | { v = CHole (k, Misctypes.IntroAnonymous, _) } -> mt()
| _ as c -> brk(0,2) ++ str" :" ++ pr_c c
- let pr_decl_notation prc ((loc,ntn),c,scopt) =
+ let pr_decl_notation prc ({loc; v=ntn},c,scopt) =
fnl () ++ keyword "where " ++ qs ntn ++ str " := "
++ Flags.without_option Flags.beautify prc c ++
pr_opt (fun sc -> str ": " ++ str sc) scopt
@@ -329,7 +331,7 @@ open Decl_kinds
let begin_of_inductive = function
| [] -> 0
- | (_,((loc,_),_))::_ -> Option.cata (fun loc -> fst (Loc.unloc loc)) 0 loc
+ | (_,({loc},_))::_ -> Option.cata (fun loc -> fst (Loc.unloc loc)) 0 loc
let pr_class_rawexpr = function
| FunClass -> keyword "Funclass"
@@ -392,8 +394,8 @@ open Decl_kinds
| SetOnlyPrinting -> keyword "only printing"
| SetOnlyParsing -> keyword "only parsing"
| SetCompatVersion v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"")
- | SetFormat("text",s) -> keyword "format " ++ pr_located qs s
- | SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_located qs s
+ | SetFormat("text",s) -> keyword "format " ++ pr_ast qs s
+ | SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_ast qs s
let pr_syntax_modifiers = function
| [] -> mt()
@@ -537,7 +539,7 @@ open Decl_kinds
let rec aux = function
| SsEmpty -> "()"
| SsType -> "(Type)"
- | SsSingl (_,id) -> "("^Id.to_string id^")"
+ | SsSingl { v=id } -> "("^Id.to_string id^")"
| SsCompl e -> "-" ^ aux e^""
| SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")"
| SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")"
@@ -661,7 +663,7 @@ open Decl_kinds
++ spc() ++ pr_smart_global q
++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
)
- | VernacInfix (((_,s),mv),q,sn) -> (* A Verifier *)
+ | VernacInfix (({v=s},mv),q,sn) -> (* A Verifier *)
return (
hov 0 (hov 0 (keyword "Infix "
++ qs s ++ str " :=" ++ pr_constrarg q) ++
@@ -670,7 +672,7 @@ open Decl_kinds
| None -> mt()
| Some sc -> spc() ++ str":" ++ spc() ++ str sc))
)
- | VernacNotation (c,((_,s),l),opt) ->
+ | VernacNotation (c,({v=s},l),opt) ->
return (
hov 2 (keyword "Notation" ++ spc() ++ qs s ++
str " :=" ++ Flags.without_option Flags.beautify pr_constrarg c ++ pr_syntax_modifiers l ++
@@ -680,7 +682,7 @@ open Decl_kinds
)
| VernacSyntaxExtension (_, (s, l)) ->
return (
- keyword "Reserved Notation" ++ spc() ++ pr_located qs s ++
+ keyword "Reserved Notation" ++ spc() ++ pr_ast qs s ++
pr_syntax_modifiers l
)
| VernacNotationAddFormat(s,k,v) ->
@@ -692,7 +694,7 @@ open Decl_kinds
| VernacDefinition ((discharge,kind),id,b) -> (* A verifier... *)
let pr_def_token dk =
keyword (
- if Name.is_anonymous (snd (fst id))
+ if Name.is_anonymous (fst id).v
then "Goal"
else Kindops.string_of_definition_object_kind dk)
in
@@ -711,7 +713,7 @@ open Decl_kinds
in
(pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body))
| ProveBody (bl,t) ->
- let typ u = if snd (fst id) = Anonymous then (assert (bl = []); u) else (str" :" ++ u) in
+ let typ u = if (fst id).v = Anonymous then (assert (bl = []); u) else (str" :" ++ u) in
(pr_binders_arg bl, typ (pr_spc_lconstr t), None) in
let (binds,typ,c) = pr_def_body b in
return (
@@ -889,16 +891,16 @@ open Decl_kinds
return (
hov 1 (
(if abst then keyword "Declare" ++ spc () else mt ()) ++
- keyword "Instance" ++
- (match instid with
- | (loc, Name id), l -> spc () ++ pr_ident_decl ((loc, id),l) ++ spc ()
- | (_, Anonymous), _ -> mt ()) ++
- pr_and_type_binders_arg sup ++
+ keyword "Instance" ++
+ (match instid with
+ | {loc; v = Name id}, l -> spc () ++ pr_ident_decl (CAst.(make ?loc id),l) ++ spc ()
+ | { v = Anonymous }, _ -> mt ()) ++
+ pr_and_type_binders_arg sup ++
str":" ++ spc () ++
(match bk with Implicit -> str "! " | Explicit -> mt ()) ++
pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++
(match props with
- | Some (true, { CAst.v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}"
+ | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}"
| Some (true,_) -> assert false
| Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p
| None -> mt()))
@@ -1031,7 +1033,7 @@ open Decl_kinds
hov 2 (
keyword "Arguments" ++ spc() ++
pr_smart_global q ++
- let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in
+ let pr_s = function None -> str"" | Some {v=s} -> str "%" ++ str s in
let pr_if b x = if b then x else str "" in
let pr_br imp x = match imp with
| Vernacexpr.Implicit -> str "[" ++ x ++ str "]"
@@ -1237,9 +1239,9 @@ let pr_vernac_flag =
(fun f a -> pr_vernac_flag f ++ spc() ++ a)
f
(pr_vernac_expr v' ++ sep_end v')
- | VernacTime (_,(_,v)) ->
+ | VernacTime (_,{v}) ->
return (keyword "Time" ++ spc() ++ pr_vernac_control v)
- | VernacRedirect (s, (_,v)) ->
+ | VernacRedirect (s, {v}) ->
return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_control v)
| VernacTimeout(n,v) ->
return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_control v)
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index fd7f1f92b..c1d8f1d37 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -33,10 +33,10 @@ val print_eval :
Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
val print_name : env -> Evd.evar_map -> reference or_by_notation ->
- Vernacexpr.univ_name_list option -> Pp.t
+ Universes.univ_name_list option -> Pp.t
val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t
val print_about : env -> Evd.evar_map -> reference or_by_notation ->
- Vernacexpr.univ_name_list option -> Pp.t
+ Universes.univ_name_list option -> Pp.t
val print_impargs : reference or_by_notation -> Pp.t
(** Pretty-printing functions for classes and coercions *)
diff --git a/printing/printmod.mli b/printing/printmod.mli
index 97ed063fe..4f15dd393 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -13,6 +13,6 @@ val printable_body : DirPath.t -> bool
val pr_mutual_inductive_body : Environ.env ->
MutInd.t -> Declarations.mutual_inductive_body ->
- Vernacexpr.univ_name_list option -> Pp.t
+ Universes.univ_name_list option -> Pp.t
val print_module : bool -> ModPath.t -> Pp.t
val print_modtype : ModPath.t -> Pp.t
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 833e34c33..0a50bcf8c 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -79,7 +79,7 @@ type proof_object = {
type proof_ending =
| Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t
| Proved of Vernacexpr.opacity_flag *
- Vernacexpr.lident option *
+ Misctypes.lident option *
proof_object
type proof_terminator = proof_ending -> unit
type closed_proof = proof_object * proof_terminator
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 29445a746..06647bf3e 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -50,7 +50,7 @@ type proof_ending =
| Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
UState.t
| Proved of Vernacexpr.opacity_flag *
- Vernacexpr.lident option *
+ Misctypes.lident option *
proof_object
type proof_terminator
type closed_proof = proof_object * proof_terminator
diff --git a/stm/stm.ml b/stm/stm.ml
index 92587b8ea..e7c371798 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -565,8 +565,8 @@ end = struct (* {{{ *)
let reachable id = reachable !vcs id
let mk_branch_name { expr = x } = Branch.make
(match Vernacprop.under_control x with
- | VernacDefinition (_,((_, Name i),_),_) -> Id.to_string i
- | VernacStartTheoremProof (_,[((_,i),_),_]) -> Id.to_string i
+ | VernacDefinition (_,({CAst.v=Name i},_),_) -> Id.to_string i
+ | VernacStartTheoremProof (_,[({CAst.v=i},_),_]) -> Id.to_string i
| _ -> "branch")
let edit_branch = Branch.make "edit"
let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind
@@ -1174,7 +1174,7 @@ end = struct (* {{{ *)
match Vernacprop.under_control v with
| VernacResetInitial ->
Stateid.initial, VtNow
- | VernacResetName (_,name) ->
+ | VernacResetName {CAst.v=name} ->
let id = VCS.get_branch_pos (VCS.current_branch ()) in
(try
let oid =
@@ -1236,7 +1236,7 @@ let set_compilation_hints file =
let get_hint_ctx loc =
let s = Aux_file.get ?loc !hints "context_used" in
let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in
- let ids = List.map (fun id -> Loc.tag id) ids in
+ let ids = List.map (fun id -> CAst.make id) ids in
match ids with
| [] -> SsEmpty
| x :: xs ->
@@ -1956,8 +1956,8 @@ end = struct (* {{{ *)
=
let e, time, batch, fail =
let rec find ~time ~batch ~fail = function
- | VernacTime (batch,(_,e)) -> find ~time:true ~batch ~fail e
- | VernacRedirect (_,(_,e)) -> find ~time ~batch ~fail e
+ | VernacTime (batch,{CAst.v=e}) -> find ~time:true ~batch ~fail e
+ | VernacRedirect (_,{CAst.v=e}) -> find ~time ~batch ~fail e
| VernacFail e -> find ~time ~batch ~fail:true e
| e -> e, time, batch, fail in
find ~time:false ~batch:false ~fail:false e in
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index cbbb54e45..93d58b2a9 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -6,10 +6,11 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Vernacexpr
open CErrors
open Util
open Pp
+open CAst
+open Vernacexpr
let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"]
@@ -87,13 +88,14 @@ let classify_vernac e =
| VernacUnsetOption (["Default";"Proof";"Using"])
| VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
(* StartProof *)
- | VernacDefinition ((Decl_kinds.DoDischarge,_),((_,i),_),ProveBody _) ->
- VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity, idents_of_name i), VtLater
- | VernacDefinition (_,((_,i),_),ProveBody _) ->
+ | VernacDefinition ((Decl_kinds.DoDischarge,_),({v=i},_),ProveBody _) ->
+ VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity, idents_of_name i), VtLater
+
+ | VernacDefinition (_,({v=i},_),ProveBody _) ->
let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
VtStartProof(default_proof_mode (),guarantee, idents_of_name i), VtLater
| VernacStartTheoremProof (_,l) ->
- let ids = List.map (fun (((_, i), _), _) -> i) l in
+ let ids = List.map (fun (({v=i}, _), _) -> i) l in
let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
VtStartProof (default_proof_mode (),guarantee,ids), VtLater
| VernacFixpoint (discharge,l) ->
@@ -102,7 +104,7 @@ let classify_vernac e =
else GuaranteesOpacity
in
let ids, open_proof =
- List.fold_left (fun (l,b) ((((_,id),_),_,_,_,p),_) ->
+ List.fold_left (fun (l,b) ((({v=id},_),_,_,_,p),_) ->
id::l, b || p = None) ([],false) l in
if open_proof
then VtStartProof (default_proof_mode (),guarantee,ids), VtLater
@@ -113,29 +115,29 @@ let classify_vernac e =
else GuaranteesOpacity
in
let ids, open_proof =
- List.fold_left (fun (l,b) ((((_,id),_),_,_,p),_) ->
+ List.fold_left (fun (l,b) ((({v=id},_),_,_,p),_) ->
id::l, b || p = None) ([],false) l in
if open_proof
then VtStartProof (default_proof_mode (),guarantee,ids), VtLater
else VtSideff ids, VtLater
(* Sideff: apply to all open branches. usually run on master only *)
| VernacAssumption (_,_,l) ->
- let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> snd id) l) l) in
- VtSideff ids, VtLater
- | VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff (idents_of_name id), VtLater
+ let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> id.v) l) l) in
+ VtSideff ids, VtLater
+ | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id), VtLater
| VernacInductive (_, _,_,l) ->
- let ids = List.map (fun (((_,((_,id),_)),_,_,_,cl),_) -> id :: match cl with
- | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l
- | RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @
+ let ids = List.map (fun (((_,({v=id},_)),_,_,_,cl),_) -> id :: match cl with
+ | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l
+ | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @
CList.map_filter (function
- | ((_,AssumExpr((_,Names.Name n),_)),_),_ -> Some n
+ | ((_,AssumExpr({v=Names.Name n},_)),_),_ -> Some n
| _ -> None) l) l in
VtSideff (List.flatten ids), VtLater
| VernacScheme l ->
- let ids = List.map snd (CList.map_filter (fun (x,_) -> x) l) in
+ let ids = List.map (fun {v}->v) (CList.map_filter (fun (x,_) -> x) l) in
VtSideff ids, VtLater
- | VernacCombinedScheme ((_,id),_) -> VtSideff [id], VtLater
- | VernacBeginSection (_,id) -> VtSideff [id], VtLater
+ | VernacCombinedScheme ({v=id},_) -> VtSideff [id], VtLater
+ | VernacBeginSection {v=id} -> VtSideff [id], VtLater
| VernacUniverse _ | VernacConstraint _
| VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _
| VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _
@@ -159,10 +161,10 @@ let classify_vernac e =
(* (Local) Notations have to disappear *)
| VernacEndSegment _ -> VtSideff [], VtNow
(* Modules with parameters have to be executed: can import notations *)
- | VernacDeclareModule (exp,(_,id),bl,_)
- | VernacDefineModule (exp,(_,id),bl,_,_) ->
+ | VernacDeclareModule (exp,{v=id},bl,_)
+ | VernacDefineModule (exp,{v=id},bl,_,_) ->
VtSideff [id], if bl = [] && exp = None then VtLater else VtNow
- | VernacDeclareModuleType ((_,id),bl,_,_) ->
+ | VernacDeclareModuleType ({v=id},bl,_,_) ->
VtSideff [id], if bl = [] then VtLater else VtNow
(* These commands alter the parser *)
| VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _
@@ -198,7 +200,7 @@ let classify_vernac e =
) poly f in
static_classifier ~poly e
| VernacTimeout (_,e) -> static_control_classifier ~poly e
- | VernacTime (_,(_,e)) | VernacRedirect (_, (_,e)) ->
+ | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) ->
static_control_classifier ~poly e
| VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
(match static_control_classifier ~poly e with
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 674d01777..9a1ac768c 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1484,7 +1484,7 @@ let simpleInjClause flags with_evars = function
| Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (injEq flags ~old:true with_evars clear_flag None)) c
let injConcl flags = injClause flags None false None
-let injHyp flags clear_flag id = injClause flags None false (Some (clear_flag,ElimOnIdent (Loc.tag id)))
+let injHyp flags clear_flag id = injClause flags None false (Some (clear_flag,ElimOnIdent CAst.(make id)))
let decompEqThen keep_proofs ntac (lbeq,_,(t,t1,t2) as u) clause =
Proofview.Goal.enter begin fun gl ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 29a30b4a2..7e281e2fe 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1190,7 +1190,7 @@ let onOpenInductionArg env sigma tac = function
let sigma = Tacmach.New.project gl in
tac clear_flag (sigma,(c,NoBindings))
end))
- | clear_flag,ElimOnIdent (_,id) ->
+ | clear_flag,ElimOnIdent {CAst.v=id} ->
(* A quantified hypothesis *)
Tacticals.New.tclTHEN
(try_intros_until_id_check id)
@@ -1206,7 +1206,7 @@ let onInductionArg tac = function
Tacticals.New.tclTHEN
(intros_until_n n)
(Tacticals.New.onLastHyp (fun c -> tac clear_flag (c,NoBindings)))
- | clear_flag,ElimOnIdent (_,id) ->
+ | clear_flag,ElimOnIdent {CAst.v=id} ->
(* A quantified hypothesis *)
Tacticals.New.tclTHEN
(try_intros_until_id_check id)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 1f681d9cf..92dee84f3 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -170,7 +170,7 @@ let rec interp_vernac ~time ~check ~interactive ~state (loc,com) =
(* The -time option is only supported from console-based
clients due to the way it prints. *)
if time then print_cmd_header ?loc com;
- let com = if time then VernacTime(time,(loc,com)) else com in
+ let com = if time then VernacTime(time, CAst.make ?loc com) else com in
interp com
with reraise ->
(* XXX: In non-interactive mode edit_at seems to do very weird
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 4a2dba859..695be74bb 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -132,7 +132,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
~program_mode poly ctx (instid, bk, cl) props ?(generalize=true)
?(tac:unit Proofview.tactic option) ?hook pri =
let env = Global.env() in
- let ((loc, instid), pl) = instid in
+ let ({CAst.loc;v=instid}, pl) = instid in
let sigma, decl = Univdecls.interp_univ_decl_opt env pl in
let tclass, ids =
match bk with
@@ -410,7 +410,7 @@ let context poly l =
let nstatus = match b with
| None ->
pi3 (ComAssumption.declare_assumption false decl (t, univs) Universes.empty_binders [] impl
- Vernacexpr.NoInline (Loc.tag id))
+ Vernacexpr.NoInline (CAst.make id))
| Some b ->
let decl = (Discharge, poly, Definition) in
let entry = Declare.definition_entry ~univs ~types:t b in
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 5d7adb24a..7e5b941ad 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -42,7 +42,7 @@ let should_axiom_into_instance = function
true
| Global | Local -> !axiom_into_instance
-let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl (_,ident) =
+let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ident} =
match local with
| Discharge when Lib.sections_are_opened () ->
let ctx = match ctx with
@@ -109,7 +109,7 @@ let declare_assumptions idl is_coe k (c,uctx) pl imps nl =
let maybe_error_many_udecls = function
- | ((loc,id), Some _) ->
+ | ({CAst.loc;v=id}, Some _) ->
user_err ?loc ~hdr:"many_universe_declarations"
Pp.(str "When declaring multiple axioms in one command, " ++
str "only the first is allowed a universe binder " ++
@@ -126,7 +126,7 @@ let process_assumptions_udecls kind l =
in
let () = match kind, udecl with
| (Discharge, _, _), Some _ when Lib.sections_are_opened () ->
- let loc = fst first_id in
+ let loc = first_id.CAst.loc in
let msg = Pp.str "Section variables cannot be polymorphic." in
user_err ?loc msg
| _ -> ()
@@ -151,8 +151,8 @@ let do_assumptions kind nl l =
let (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) ->
let sigma,(t,imps) = interp_assumption sigma env ienv [] c in
let env =
- push_named_context (List.map (fun (_,id) -> LocalAssum (id,t)) idl) env in
- let ienv = List.fold_right (fun (_,id) ienv ->
+ push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (id,t)) idl) env in
+ let ienv = List.fold_right (fun {CAst.v=id} ienv ->
let impls = compute_internalization_data env Variable t imps in
Id.Map.add id impls ienv) idl ienv in
((sigma,env,ienv),((is_coe,idl),t,imps)))
@@ -175,7 +175,7 @@ let do_assumptions kind nl l =
let t = replace_vars subst t in
let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in
let subst' = List.map2
- (fun (_,id) (c,u) -> (id, Universes.constr_of_global_univ (c,u)))
+ (fun {CAst.v=id} (c,u) -> (id, Universes.constr_of_global_univ (c,u)))
idl refs
in
subst'@subst, status' && status, next_uctx uctx)
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 2fa156abd..0491638c9 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -30,5 +30,5 @@ val do_assumptions : locality * polymorphic * assumption_object_kind ->
val declare_assumption : coercion_flag -> assumption_kind ->
types in_constant_universes_entry ->
Universes.universe_binders -> Impargs.manual_implicits ->
- bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located ->
+ bool (** implicit *) -> Vernacexpr.inline -> variable CAst.t ->
global_reference * Univ.Instance.t * bool
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index d648e293a..489f299a2 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -102,7 +102,7 @@ let check_mutuality env evd isfix fixl =
type structured_fixpoint_expr = {
fix_name : Id.t;
fix_univs : universe_decl_expr option;
- fix_annot : Id.t Loc.located option;
+ fix_annot : lident option;
fix_binders : local_binder_expr list;
fix_body : constr_expr option;
fix_type : constr_expr
@@ -175,7 +175,7 @@ let interp_recursive ~program_mode ~cofix fixl notations =
| x , None -> x
| Some ls , Some us ->
let lsu = ls.univdecl_instance and usu = us.univdecl_instance in
- if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) lsu usu) then
+ if not (CList.for_all2eq (fun x y -> Id.equal x.CAst.v y.CAst.v) lsu usu) then
user_err Pp.(str "(co)-recursive definitions should all have the same universe binders");
Some us) fixl None in
let sigma, decl = Univdecls.interp_univ_decl_opt env all_universes in
@@ -323,7 +323,7 @@ let extract_decreasing_argument limit = function
let extract_fixpoint_components limit l =
let fixl, ntnl = List.split l in
- let fixl = List.map (fun (((_,id),pl),ann,bl,typ,def) ->
+ let fixl = List.map (fun (({CAst.v=id},pl),ann,bl,typ,def) ->
let ann = extract_decreasing_argument limit ann in
{fix_name = id; fix_annot = ann; fix_univs = pl;
fix_binders = bl; fix_body = def; fix_type = typ}) fixl in
@@ -331,7 +331,7 @@ let extract_fixpoint_components limit l =
let extract_cofixpoint_components l =
let fixl, ntnl = List.split l in
- List.map (fun (((_,id),pl),bl,typ,def) ->
+ List.map (fun (({CAst.v=id},pl),bl,typ,def) ->
{fix_name = id; fix_annot = None; fix_univs = pl;
fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
List.flatten ntnl
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 2c84bd84d..2926e30e5 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -31,7 +31,7 @@ val do_cofixpoint :
type structured_fixpoint_expr = {
fix_name : Id.t;
fix_univs : Vernacexpr.universe_decl_expr option;
- fix_annot : Id.t Loc.located option;
+ fix_annot : Misctypes.lident option;
fix_binders : local_binder_expr list;
fix_body : constr_expr option;
fix_type : constr_expr
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 41474fc63..c650e9e40 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -249,7 +249,7 @@ let inductive_levels env evd poly arities inds =
(evd,[]) (Array.to_list levels') destarities sizes
in evd, List.rev arities
-let check_named (loc, na) = match na with
+let check_named {CAst.loc;v=na} = match na with
| Name _ -> ()
| Anonymous ->
let msg = str "Parameters must be named." in
@@ -260,7 +260,7 @@ let check_param = function
| CLocalDef (na, _, _) -> check_named na
| CLocalAssum (nas, Default _, _) -> List.iter check_named nas
| CLocalAssum (nas, Generalized _, _) -> ()
-| CLocalPattern (loc,_) ->
+| CLocalPattern {CAst.loc} ->
Loc.raise ?loc (Stream.Error "pattern with quote not allowed here.")
let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
@@ -364,7 +364,7 @@ let eq_local_binders bl1 bl2 =
List.equal local_binder_eq bl1 bl2
let extract_coercions indl =
- let mkqid (_,((_,id),_)) = qualid_of_ident id in
+ let mkqid (_,({CAst.v=id},_)) = qualid_of_ident id in
let extract lc = List.filter (fun (iscoe,_) -> iscoe) lc in
List.map mkqid (List.flatten(List.map (fun (_,_,_,lc) -> extract lc) indl))
@@ -378,10 +378,10 @@ let extract_params indl =
params
let extract_inductive indl =
- List.map (fun (((_,indname),pl),_,ar,lc) -> {
+ List.map (fun (({CAst.v=indname},pl),_,ar,lc) -> {
ind_name = indname; ind_univs = pl;
ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (GType [])) ar;
- ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc
+ ind_lc = List.map (fun (_,({CAst.v=id},t)) -> (id,t)) lc
}) indl
let extract_mutual_inductive_declaration_components indl =
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index a9a91e304..af34f8b29 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -298,16 +298,16 @@ let do_program_recursive local poly fixkind fixl ntns =
let do_program_fixpoint local poly l =
let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
match g, l with
- | [(n, CWfRec r)], [((((_,id),pl),_,bl,typ,def),ntn)] ->
+ | [(n, CWfRec r)], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
let recarg =
match n with
- | Some n -> mkIdentC (snd n)
+ | Some n -> mkIdentC n.CAst.v
| None ->
user_err ~hdr:"do_program_fixpoint"
(str "Recursive argument required for well-founded fixpoints")
in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn
- | [(n, CMeasureRec (m, r))], [((((_,id),pl),_,bl,typ,def),ntn)] ->
+ | [(n, CMeasureRec (m, r))], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
build_wellfounded (id, pl, n, bl, typ, out_def def) poly
(Option.default (CAst.make @@ CRef (lt_ref,None)) r) m ntn
@@ -322,7 +322,7 @@ let do_program_fixpoint local poly l =
let extract_cofixpoint_components l =
let fixl, ntnl = List.split l in
- List.map (fun (((_,id),pl),bl,typ,def) ->
+ List.map (fun (({CAst.v=id},pl),bl,typ,def) ->
{fix_name = id; fix_annot = None; fix_univs = pl;
fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
List.flatten ntnl
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 2f4c95aff..447c5085b 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -367,17 +367,16 @@ requested
| InType -> recs ^ "t_nodep")
) in
let newid = add_suffix (basename_of_global (IndRef ind)) suffix in
- let newref = Loc.tag newid in
+ let newref = CAst.make newid in
((newref,isdep,ind,z)::l1),l2
in
match t with
| CaseScheme (x,y,z) -> names "_case" "_case" x y z
| InductionScheme (x,y,z) -> names "_ind" "_rec" x y z
| EqualityScheme x -> l1,((None,smart_global_inductive x)::l2)
-
let do_mutual_induction_scheme lnamedepindsort =
- let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort
+ let lrecnames = List.map (fun ({CAst.v},_,_,_) -> v) lnamedepindsort
and env0 = Global.env() in
let sigma, lrecspec, _ =
List.fold_right
@@ -416,7 +415,7 @@ let get_common_underlying_mutual_inductive = function
then user_err Pp.(str "A type occurs twice");
mind,
List.map_filter
- (function (Some id,(_,i)) -> Some (i,snd id) | (None,_) -> None) all
+ (function (Some id,(_,i)) -> Some (i,id.CAst.v) | (None,_) -> None) all
let do_scheme l =
let ischeme,escheme = split_scheme l in
@@ -450,7 +449,7 @@ let fold_left' f = function
let mk_coq_and sigma = Evarutil.new_global sigma (Coqlib.build_coq_and ())
let mk_coq_conj sigma = Evarutil.new_global sigma (Coqlib.build_coq_conj ())
-
+
let build_combined_scheme env schemes =
let evdref = ref (Evd.from_env env) in
let defs = List.map (fun cst ->
@@ -492,18 +491,19 @@ let build_combined_scheme env schemes =
(!evdref, body, typ)
let do_combined_scheme name schemes =
+ let open CAst in
let csts =
- List.map (fun x ->
- let refe = Ident x in
- let qualid = qualid_of_reference refe in
- try Nametab.locate_constant (snd qualid)
- with Not_found -> user_err Pp.(pr_qualid (snd qualid) ++ str " is not declared."))
+ List.map (fun {CAst.loc;v} ->
+ let refe = Ident (Loc.tag ?loc v) in
+ let qualid = qualid_of_reference refe in
+ try Nametab.locate_constant (snd qualid)
+ with Not_found -> user_err Pp.(pr_qualid (snd qualid) ++ str " is not declared."))
schemes
in
let sigma,body,typ = build_combined_scheme (Global.env ()) csts in
let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
- ignore (define (snd name) UserIndividualRequest sigma proof_output (Some typ));
- fixpoint_message None [snd name]
+ ignore (define name.v UserIndividualRequest sigma proof_output (Some typ));
+ fixpoint_message None [name.v]
(**********************************************************************)
diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli
index 4b31389ab..8658d85f6 100644
--- a/vernac/indschemes.mli
+++ b/vernac/indschemes.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Loc
open Names
open Constr
open Environ
@@ -31,17 +30,17 @@ val declare_rewriting_schemes : inductive -> unit
(** Mutual Minimality/Induction scheme *)
val do_mutual_induction_scheme :
- (Id.t located * bool * inductive * Sorts.family) list -> unit
+ (Misctypes.lident * bool * inductive * Sorts.family) list -> unit
(** Main calls to interpret the Scheme command *)
-val do_scheme : (Id.t located option * scheme) list -> unit
+val do_scheme : (Misctypes.lident option * scheme) list -> unit
(** Combine a list of schemes into a conjunction of them *)
val build_combined_scheme : env -> Constant.t list -> Evd.evar_map * constr * types
-val do_combined_scheme : Id.t located -> Id.t located list -> unit
+val do_combined_scheme : Misctypes.lident -> Misctypes.lident list -> unit
(** Hook called at each inductive type definition *)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 57436784b..7661fff6d 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -214,7 +214,7 @@ let fresh_name_for_anonymous_theorem () =
let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in
next_global_ident_away default_thm_id avoid
-let check_name_freshness locality (loc,id) : unit =
+let check_name_freshness locality {CAst.loc;v=id} : unit =
(* We check existence here: it's a bit late at Qed time *)
if Nametab.exists_cci (Lib.make_path id) || is_section_variable id ||
locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
@@ -339,7 +339,7 @@ let universe_proof_terminator compute_guard hook =
(hook (Some (proof.Proof_global.universes))) is_opaque in
begin match idopt with
| None -> save_named ~export_seff proof
- | Some (_,id) -> save_anonymous ~export_seff proof id
+ | Some { CAst.v = id } -> save_anonymous ~export_seff proof id
end
end
@@ -444,7 +444,7 @@ let start_proof_com ?inference_hook kind thms hook =
let ids = List.map RelDecl.get_name ctx in
check_name_freshness (pi1 kind) id;
(* XXX: The nf_evar is critical !! *)
- evd, (snd id,
+ evd, (id.CAst.v,
(Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx),
(ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps'))))
evd thms in
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index bcffe640c..f63206216 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -89,7 +89,7 @@ let pr_grammar = function
(* Parse a format (every terminal starting with a letter or a single
quote (except a single quote alone) must be quoted) *)
-let parse_format ((loc, str) : lstring) =
+let parse_format ({CAst.loc;v=str} : Misctypes.lstring) =
let len = String.length str in
(* TODO: update the line of the location when the string contains newlines *)
let make_loc i j = Option.map (Loc.shift_loc (i+1) (j-len)) loc in
@@ -789,7 +789,7 @@ type notation_modifier = {
only_parsing : bool;
only_printing : bool;
compat : Flags.compat_version option;
- format : string Loc.located option;
+ format : Misctypes.lstring option;
extra : (string * string) list;
}
@@ -847,7 +847,7 @@ let interp_modifiers modl = let open NotationMods in
| SetFormat ("text",s) :: l ->
if not (Option.is_empty acc.format) then user_err Pp.(str "A format is given more than once.");
interp { acc with format = Some s; } l
- | SetFormat (k,(_,s)) :: l ->
+ | SetFormat (k,{CAst.v=s}) :: l ->
interp { acc with extra = (k,s)::acc.extra; } l
in interp default modl
@@ -1101,7 +1101,7 @@ module SynData = struct
only_parsing : bool;
only_printing : bool;
compat : Flags.compat_version option;
- format : string Loc.located option;
+ format : Misctypes.lstring option;
extra : (string * string) list;
(* XXX: Callback to printing, must remove *)
@@ -1400,7 +1400,7 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_
(* Notations without interpretation (Reserved Notation) *)
-let add_syntax_extension local ((loc,df),mods) = let open SynData in
+let add_syntax_extension local ({CAst.loc;v=df},mods) = let open SynData in
let psd = compute_pure_syntax_data df mods in
let sy_rules = make_syntax_rules {psd with compat = None} in
Flags.if_verbose (List.iter (fun (f,x) -> f x)) psd.msgs;
@@ -1408,11 +1408,11 @@ let add_syntax_extension local ((loc,df),mods) = let open SynData in
(* Notations with only interpretation *)
-let add_notation_interpretation env ((loc,df),c,sc) =
+let add_notation_interpretation env ({CAst.loc;v=df},c,sc) =
let df' = add_notation_interpretation_core false df env c sc false false None in
Dumpglob.dump_notation (loc,df') sc true
-let set_notation_for_interpretation env impls ((_,df),c,sc) =
+let set_notation_for_interpretation env impls ({CAst.v=df},c,sc) =
(try ignore
(Flags.silently (fun () -> add_notation_interpretation_core false df env ~impls c sc false false None) ());
with NoSyntaxRule ->
@@ -1421,7 +1421,7 @@ let set_notation_for_interpretation env impls ((_,df),c,sc) =
(* Main entry point *)
-let add_notation local env c ((loc,df),modifiers) sc =
+let add_notation local env c ({CAst.loc;v=df},modifiers) sc =
let df' =
if no_syntax_modifiers modifiers then
(* No syntax data: try to rely on a previously declared rule *)
@@ -1448,13 +1448,13 @@ let add_notation_extra_printing_rule df k v =
let inject_var x = CAst.make @@ CRef (Ident (Loc.tag @@ Id.of_string x),None)
-let add_infix local env ((loc,inf),modifiers) pr sc =
+let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc =
check_infix_modifiers modifiers;
(* check the precedence *)
let metas = [inject_var "x"; inject_var "y"] in
let c = mkAppC (pr,metas) in
- let df = "x "^(quote_notation_token inf)^" y" in
- add_notation local env c ((loc,df),modifiers) sc
+ let df = CAst.make ?loc @@ "x "^(quote_notation_token inf)^" y" in
+ add_notation local env c (df,modifiers) sc
(**********************************************************************)
(* Delimiters and classes bound to scopes *)
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index 9137f7a7e..7740604c3 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -12,6 +12,7 @@ open Notation
open Constrexpr
open Notation_term
open Environ
+open Misctypes
val add_token_obj : string -> unit
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 58e4b00fc..e4bcbc4bb 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -295,10 +295,10 @@ type obligation =
type obligations = (obligation array * int)
type fixpoint_kind =
- | IsFixpoint of (Id.t Loc.located option * Constrexpr.recursion_order_expr) list
+ | IsFixpoint of (Misctypes.lident option * Constrexpr.recursion_order_expr) list
| IsCoFixpoint
-type notations = (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
+type notations = (Misctypes.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
type program_info_aux = {
prg_name: Id.t;
@@ -500,7 +500,7 @@ let rec lam_index n t acc =
let compute_possible_guardness_evidences (n,_) fixbody fixtype =
match n with
- | Some (loc, n) -> [lam_index n fixbody 0]
+ | Some { CAst.loc; v = n } -> [lam_index n fixbody 0]
| None ->
(* If recursive argument was not given by user, we try all args.
An earlier approach was to look only for inductive arguments,
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index bdc97d48c..0ec127152 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -61,10 +61,10 @@ val add_definition : Names.Id.t -> ?term:constr -> types ->
?hook:(UState.t -> unit) Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress
type notations =
- (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
+ (Misctypes.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
type fixpoint_kind =
- | IsFixpoint of (Id.t Loc.located option * Constrexpr.recursion_order_expr) list
+ | IsFixpoint of (Misctypes.lident option * Constrexpr.recursion_order_expr) list
| IsCoFixpoint
val add_mutual_definitions :
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index ffe99cfd8..8422baf57 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -51,7 +51,7 @@ let rec process_expr env e ty =
let rec aux = function
| SsEmpty -> Id.Set.empty
| SsType -> set_of_type env ty
- | SsSingl (_,id) -> set_of_id env id
+ | SsSingl { CAst.v = id } -> set_of_id env id
| SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2)
| SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2)
| SsCompl e -> Id.Set.diff (full_set env) (aux e)
diff --git a/vernac/record.ml b/vernac/record.ml
index 16b95a5ef..1140e3d37 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -62,7 +62,7 @@ let _ =
let interp_fields_evars env sigma impls_env nots l =
List.fold_left2
- (fun (env, sigma, uimpls, params, impls) no ((loc, i), b, t) ->
+ (fun (env, sigma, uimpls, params, impls) no ({CAst.loc;v=i}, b, t) ->
let sigma, (t', impl) = interp_type_evars_impls env sigma ~impls t in
let sigma, b' =
Option.cata (fun x -> on_snd (fun x -> Some (fst x)) @@
@@ -92,8 +92,9 @@ let compute_constructor_level evars env l =
let binder_of_decl = function
| Vernacexpr.AssumExpr(n,t) -> (n,None,t)
- | Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c
- | None -> CAst.make ?loc:(fst n) @@ CHole (None, Misctypes.IntroAnonymous, None))
+ | Vernacexpr.DefExpr(n,c,t) ->
+ (n,Some c, match t with Some c -> c
+ | None -> CAst.make ?loc:n.CAst.loc @@ CHole (None, Misctypes.IntroAnonymous, None))
let binders_of_decls = List.map binder_of_decl
@@ -101,7 +102,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs =
let env0 = Global.env () in
let sigma, decl = Univdecls.interp_univ_decl_opt env0 pl in
let _ =
- let error bk (loc, name) =
+ let error bk {CAst.loc; v=name} =
match bk, name with
| Default _, Anonymous ->
user_err ?loc ~hdr:"record" (str "Record parameters must be named")
@@ -110,7 +111,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs =
List.iter
(function CLocalDef (b, _, _) -> error default_binder_kind b
| CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls
- | CLocalPattern (loc,(_,_)) ->
+ | CLocalPattern {CAst.loc} ->
Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps
in
let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars env0 sigma ps in
@@ -571,13 +572,13 @@ open Vernacexpr
(* [fs] corresponds to fields and [ps] to parameters; [coers] is a
list telling if the corresponding fields must me declared as coercions
or subinstances. *)
-let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) =
+let definition_structure (kind,cum,poly,finite,(is_coe,({CAst.loc;v=idstruc},pl)),ps,cfs,idbuild,s) =
let cfs,notations = List.split cfs in
let cfs,priorities = List.split cfs in
let coers,fs = List.split cfs in
let extract_name acc = function
- Vernacexpr.AssumExpr((_,Name id),_) -> id::acc
- | Vernacexpr.DefExpr ((_,Name id),_,_) -> id::acc
+ Vernacexpr.AssumExpr({CAst.v=Name id},_) -> id::acc
+ | Vernacexpr.DefExpr ({CAst.v=Name id},_,_) -> id::acc
| _ -> acc in
let allnames = idstruc::(List.fold_left extract_name [] fs) in
let () = match List.duplicates Id.equal allnames with
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index fa457c895..689d7a423 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -10,6 +10,7 @@
open Pp
open CErrors
+open CAst
open Util
open Names
open Nameops
@@ -471,13 +472,13 @@ let vernac_definition_hook p = function
| SubClass -> Class.add_subclass_hook p
| _ -> no_hook
-let vernac_definition ~atts discharge kind ((loc, id), pl) def =
+let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def =
let local = enforce_locality_exp atts.locality discharge in
let hook = vernac_definition_hook atts.polymorphic kind in
let () =
match id with
| Anonymous -> ()
- | Name n -> let lid = (loc, n) in
+ | Name n -> let lid = CAst.make ?loc n in
match local with
| Discharge -> Dumpglob.dump_definition lid true "var"
| Local | Global -> Dumpglob.dump_definition lid false "def"
@@ -491,7 +492,7 @@ let vernac_definition ~atts discharge kind ((loc, id), pl) def =
(match def with
| ProveBody (bl,t) -> (* local binders, typ *)
start_proof_and_print (local, atts.polymorphic, DefinitionBody kind)
- [((loc, name), pl), (bl, t)] hook
+ [(CAst.make ?loc name, pl), (bl, t)] hook
| DefineBody (bl,red_option,c,typ_opt) ->
let red_option = match red_option with
| None -> None
@@ -546,14 +547,14 @@ let should_treat_as_cumulative cum poly =
let vernac_record cum k poly finite struc binders sort nameopt cfs =
let is_cumulative = should_treat_as_cumulative cum poly in
let const = match nameopt with
- | None -> add_prefix "Build_" (snd (fst (snd struc)))
- | Some (_,id as lid) ->
+ | None -> add_prefix "Build_" (fst (snd struc)).v
+ | Some ({v=id} as lid) ->
Dumpglob.dump_definition lid false "constr"; id in
if Dumpglob.dump () then (
Dumpglob.dump_definition (fst (snd struc)) false "rec";
List.iter (fun (((_, x), _), _) ->
match x with
- | Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
+ | Vernacexpr.AssumExpr ({loc;v=Name id}, _) -> Dumpglob.dump_definition (make ?loc id) false "proj"
| _ -> ()) cfs);
ignore(Record.definition_structure (k,is_cumulative,poly,finite,struc,binders,cfs,const,sort))
@@ -582,9 +583,9 @@ let vernac_inductive ~atts cum lo finite indl =
atts.polymorphic finite id bl c oc fs
| [ ( id , bl , c , Class _, Constructors [l]), [] ] ->
let f =
- let (coe, ((loc, id), ce)) = l in
+ let (coe, ({loc;v=id}, ce)) = l in
let coe' = if coe then Some true else None in
- (((coe', AssumExpr ((loc, Name id), ce)), None), [])
+ (((coe', AssumExpr ((make ?loc @@ Name id), ce)), None), [])
in vernac_record cum (Class true) atts.polymorphic finite id bl c None [f]
| [ ( _ , _, _, Class _, Constructors _), [] ] ->
user_err Pp.(str "Inductive classes not supported")
@@ -637,7 +638,7 @@ let vernac_scheme l =
let vernac_combined_scheme lid l =
if Dumpglob.dump () then
(Dumpglob.dump_definition lid false "def";
- List.iter (fun lid -> dump_global (Misctypes.AN (Ident lid))) l);
+ List.iter (fun {loc;v=id} -> dump_global (Misctypes.AN (Ident (Loc.tag ?loc id)))) l);
Indschemes.do_combined_scheme lid l
let vernac_universe ~atts l =
@@ -660,7 +661,7 @@ let vernac_constraint ~atts l =
let vernac_import export refl =
Library.import_module export (List.map qualid_of_reference refl)
-let vernac_declare_module export (loc, id) binders_ast mty_ast =
+let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
(* We check the state of the system (in section, in module type)
and what module information is supplied *)
if Lib.sections_are_opened () then
@@ -678,7 +679,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast =
Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared");
Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)]) export
-let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
+let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l =
(* We check the state of the system (in section, in module type)
and what module information is supplied *)
if Lib.sections_are_opened () then
@@ -689,7 +690,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
let binders_ast,argsexport =
List.fold_right
(fun (export,idl,ty) (args,argsexport) ->
- (idl,ty)::args, (List.map (fun (_,i) -> export,i)idl)@argsexport) binders_ast
+ (idl,ty)::args, (List.map (fun {v=i} -> export,i)idl)@argsexport) binders_ast
([],[]) in
let mp =
Declaremods.start_module Modintern.interp_module_ast
@@ -719,13 +720,13 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)])
export
-let vernac_end_module export (loc,id as lid) =
+let vernac_end_module export {loc;v=id} =
let mp = Declaremods.end_module () in
Dumpglob.dump_modref ?loc mp "mod";
Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined");
- Option.iter (fun export -> vernac_import export [Ident lid]) export
+ Option.iter (fun export -> vernac_import export [Ident (Loc.tag ?loc id)]) export
-let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
+let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l =
if Lib.sections_are_opened () then
user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
@@ -735,7 +736,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
let binders_ast,argsexport =
List.fold_right
(fun (export,idl,ty) (args,argsexport) ->
- (idl,ty)::args, (List.map (fun (_,i) -> export,i)idl)@argsexport) binders_ast
+ (idl,ty)::args, (List.map (fun {v=i} -> export,i)idl)@argsexport) binders_ast
([],[]) in
let mp =
@@ -765,7 +766,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
Flags.if_verbose Feedback.msg_info
(str "Module Type " ++ Id.print id ++ str " is defined")
-let vernac_end_modtype (loc,id) =
+let vernac_end_modtype {loc;v=id} =
let mp = Declaremods.end_modtype () in
Dumpglob.dump_modref ?loc mp "modtype";
Flags.if_verbose Feedback.msg_info (str "Module Type " ++ Id.print id ++ str " is defined")
@@ -778,21 +779,21 @@ let vernac_include l =
(* Sections *)
-let vernac_begin_section (_, id as lid) =
+let vernac_begin_section ({v=id} as lid) =
Proof_global.check_no_pending_proof ();
Dumpglob.dump_definition lid true "sec";
Lib.open_section id
-let vernac_end_section (loc,_) =
+let vernac_end_section {CAst.loc} =
Dumpglob.dump_reference ?loc
(DirPath.to_string (Lib.current_dirpath true)) "<>" "sec";
Lib.close_section ()
-let vernac_name_sec_hyp (_,id) set = Proof_using.name_set id set
+let vernac_name_sec_hyp {v=id} set = Proof_using.name_set id set
(* Dispatcher of the "End" command *)
-let vernac_end_segment (_,id as lid) =
+let vernac_end_segment ({v=id} as lid) =
Proof_global.check_no_pending_proof ();
match Lib.find_opening_node id with
| Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid
@@ -975,7 +976,7 @@ let vernac_hints ~atts lb h =
let vernac_syntactic_definition ~atts lid x y =
Dumpglob.dump_definition lid false "syndef";
let local = enforce_module_locality atts.locality in
- Metasyntax.add_syntactic_definition (Global.env()) (snd lid) x local y
+ Metasyntax.add_syntactic_definition (Global.env()) lid.v x local y
let vernac_declare_implicits ~atts r l =
let local = make_section_locality atts.locality in
@@ -1211,7 +1212,7 @@ let vernac_arguments ~atts reference args more_implicits nargs_for_red flags =
end;
if scopes_specified || clear_scopes_flag then begin
- let scopes = List.map (Option.map (fun (loc,k) ->
+ let scopes = List.map (Option.map (fun {loc;v=k} ->
try ignore (Notation.find_scope k); k
with UserError _ ->
Notation.find_delimiters_scope ?loc k)) scopes
@@ -1824,7 +1825,7 @@ let vernac_locate = function
let vernac_register id r =
if Proof_global.there_are_pending_proofs () then
user_err Pp.(str "Cannot register a primitive while in proof editing mode.");
- let kn = Constrintern.global_reference (snd id) in
+ let kn = Constrintern.global_reference id.v in
if not (isConstRef kn) then
user_err Pp.(str "Register inline: a constant is expected");
match r with
@@ -2015,7 +2016,7 @@ let interp ?proof ~atts ~st c =
| VernacImport (export,qidl) -> vernac_import export qidl
| VernacCanonical qid -> vernac_canonical qid
| VernacCoercion (r,s,t) -> vernac_coercion ~atts r s t
- | VernacIdentityCoercion ((_,id),s,t) ->
+ | VernacIdentityCoercion ({v=id},s,t) ->
vernac_identity_coercion ~atts id s t
(* Type classes *)
@@ -2233,12 +2234,12 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
aux ~polymorphism ~atts v
| VernacFail v -> with_fail st true (fun () -> control v)
| VernacTimeout (n,v) ->
- current_timeout := Some n;
- control v
- | VernacRedirect (s, (_,v)) ->
- Topfmt.with_output_to_file s control v
- | VernacTime (batch, (_loc,v)) ->
- System.with_time ~batch control v;
+ current_timeout := Some n;
+ control v
+ | VernacRedirect (s, {v}) ->
+ Topfmt.with_output_to_file s control v
+ | VernacTime (batch, {v}) ->
+ System.with_time ~batch control v;
and aux ~polymorphism ~atts : _ -> unit =
function
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index 3932d1c7b..172a20b7a 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -13,15 +13,15 @@ open Vernacexpr
let rec under_control = function
| VernacExpr (_, c) -> c
- | VernacRedirect (_,(_,c))
- | VernacTime (_,(_,c))
+ | VernacRedirect (_,{CAst.v=c})
+ | VernacTime (_,{CAst.v=c})
| VernacFail c
| VernacTimeout (_,c) -> under_control c
let rec has_Fail = function
| VernacExpr _ -> false
- | VernacRedirect (_,(_,c))
- | VernacTime (_,(_,c))
+ | VernacRedirect (_,{CAst.v=c})
+ | VernacTime (_,{CAst.v=c})
| VernacTimeout (_,c) -> has_Fail c
| VernacFail _ -> true
@@ -38,8 +38,8 @@ let is_navigation_vernac c =
is_navigation_vernac_expr (under_control c)
let rec is_deep_navigation_vernac = function
- | VernacTime (_,(_,c)) -> is_deep_navigation_vernac c
- | VernacRedirect (_, (_,c))
+ | VernacTime (_,{CAst.v=c}) -> is_deep_navigation_vernac c
+ | VernacRedirect (_, {CAst.v=c})
| VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c
| VernacExpr _ -> false