aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/g_ltac2.ml4302
-rw-r--r--src/tac2core.ml31
-rw-r--r--src/tac2entries.ml94
-rw-r--r--src/tac2entries.mli11
-rw-r--r--src/tac2expr.mli24
-rw-r--r--src/tac2intern.ml173
-rw-r--r--src/tac2intern.mli3
-rw-r--r--src/tac2qexpr.mli99
-rw-r--r--src/tac2quote.ml129
-rw-r--r--src/tac2quote.mli17
-rw-r--r--src/tac2tactics.ml24
11 files changed, 447 insertions, 460 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 31eb6d9db5..f4818f4ece 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -93,17 +93,17 @@ let tac2mode = Gram.entry_create "vernac:ltac2_command"
let ltac1_expr = Pltac.tactic_expr
-let inj_wit wit loc x = Loc.tag ~loc @@ CTacExt (wit, x)
+let inj_wit wit loc x = CAst.make ~loc @@ CTacExt (wit, x)
let inj_open_constr loc c = inj_wit Tac2quote.wit_open_constr loc c
let inj_pattern loc c = inj_wit Tac2quote.wit_pattern loc c
let inj_reference loc c = inj_wit Tac2quote.wit_reference loc c
let inj_ltac1 loc e = inj_wit Tac2quote.wit_ltac1 loc e
let pattern_of_qualid ?loc id =
- if Tac2env.is_constructor (snd id) then Loc.tag ?loc @@ CPatRef (RelId id, [])
+ if Tac2env.is_constructor id.CAst.v then CAst.make ?loc @@ CPatRef (RelId id, [])
else
- let (dp, id) = Libnames.repr_qualid (snd id) in
- if DirPath.is_empty dp then Loc.tag ?loc @@ CPatVar (Name id)
+ let (dp, id) = Libnames.repr_qualid id.CAst.v in
+ if DirPath.is_empty dp then CAst.make ?loc @@ CPatVar (Name id)
else
CErrors.user_err ?loc (Pp.str "Syntax error")
@@ -113,73 +113,73 @@ GEXTEND Gram
tac2pat:
[ "1" LEFTA
[ id = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" ->
- if Tac2env.is_constructor (snd id) then
- Loc.tag ~loc:!@loc @@ CPatRef (RelId id, pl)
+ if Tac2env.is_constructor (id.CAst.v) then
+ CAst.make ~loc:!@loc @@ CPatRef (RelId id, pl)
else
CErrors.user_err ~loc:!@loc (Pp.str "Syntax error")
| id = Prim.qualid -> pattern_of_qualid ~loc:!@loc id
- | "["; "]" -> Loc.tag ~loc:!@loc @@ CPatRef (AbsKn (Other Tac2core.Core.c_nil), [])
+ | "["; "]" -> CAst.make ~loc:!@loc @@ CPatRef (AbsKn (Other Tac2core.Core.c_nil), [])
| p1 = tac2pat; "::"; p2 = tac2pat ->
- Loc.tag ~loc:!@loc @@ CPatRef (AbsKn (Other Tac2core.Core.c_cons), [p1; p2])
+ CAst.make ~loc:!@loc @@ CPatRef (AbsKn (Other Tac2core.Core.c_cons), [p1; p2])
]
| "0"
- [ "_" -> Loc.tag ~loc:!@loc @@ CPatVar Anonymous
- | "()" -> Loc.tag ~loc:!@loc @@ CPatRef (AbsKn (Tuple 0), [])
+ [ "_" -> CAst.make ~loc:!@loc @@ CPatVar Anonymous
+ | "()" -> CAst.make ~loc:!@loc @@ CPatRef (AbsKn (Tuple 0), [])
| id = Prim.qualid -> pattern_of_qualid ~loc:!@loc id
| "("; p = atomic_tac2pat; ")" -> p
] ]
;
atomic_tac2pat:
[ [ ->
- Loc.tag ~loc:!@loc @@ CPatRef (AbsKn (Tuple 0), [])
+ CAst.make ~loc:!@loc @@ CPatRef (AbsKn (Tuple 0), [])
| p = tac2pat; ":"; t = tac2type ->
- Loc.tag ~loc:!@loc @@ CPatCnv (p, t)
+ CAst.make ~loc:!@loc @@ CPatCnv (p, t)
| p = tac2pat; ","; pl = LIST0 tac2pat SEP "," ->
let pl = p :: pl in
- Loc.tag ~loc:!@loc @@ CPatRef (AbsKn (Tuple (List.length pl)), pl)
+ CAst.make ~loc:!@loc @@ CPatRef (AbsKn (Tuple (List.length pl)), pl)
| p = tac2pat -> p
] ]
;
tac2expr:
[ "6" RIGHTA
- [ e1 = SELF; ";"; e2 = SELF -> Loc.tag ~loc:!@loc @@ CTacSeq (e1, e2) ]
+ [ e1 = SELF; ";"; e2 = SELF -> CAst.make ~loc:!@loc @@ CTacSeq (e1, e2) ]
| "5"
[ "fun"; it = LIST1 input_fun ; "=>"; body = tac2expr LEVEL "6" ->
- Loc.tag ~loc:!@loc @@ CTacFun (it, body)
+ CAst.make ~loc:!@loc @@ CTacFun (it, body)
| "let"; isrec = rec_flag;
lc = LIST1 let_clause SEP "with"; "in";
e = tac2expr LEVEL "6" ->
- Loc.tag ~loc:!@loc @@ CTacLet (isrec, lc, e)
+ CAst.make ~loc:!@loc @@ CTacLet (isrec, lc, e)
| "match"; e = tac2expr LEVEL "5"; "with"; bl = branches; "end" ->
- Loc.tag ~loc:!@loc @@ CTacCse (e, bl)
+ CAst.make ~loc:!@loc @@ CTacCse (e, bl)
]
| "4" LEFTA [ ]
| "::" RIGHTA
[ e1 = tac2expr; "::"; e2 = tac2expr ->
- Loc.tag ~loc:!@loc @@ CTacApp (Loc.tag ~loc:!@loc @@ CTacCst (AbsKn (Other Tac2core.Core.c_cons)), [e1; e2])
+ CAst.make ~loc:!@loc @@ CTacApp (CAst.make ~loc:!@loc @@ CTacCst (AbsKn (Other Tac2core.Core.c_cons)), [e1; e2])
]
| [ e0 = SELF; ","; el = LIST1 NEXT SEP "," ->
let el = e0 :: el in
- Loc.tag ~loc:!@loc @@ CTacApp (Loc.tag ~loc:!@loc @@ CTacCst (AbsKn (Tuple (List.length el))), el) ]
+ CAst.make ~loc:!@loc @@ CTacApp (CAst.make ~loc:!@loc @@ CTacCst (AbsKn (Tuple (List.length el))), el) ]
| "1" LEFTA
[ e = tac2expr; el = LIST1 tac2expr LEVEL "0" ->
- Loc.tag ~loc:!@loc @@ CTacApp (e, el)
+ CAst.make ~loc:!@loc @@ CTacApp (e, el)
| e = SELF; ".("; qid = Prim.qualid; ")" ->
- Loc.tag ~loc:!@loc @@ CTacPrj (e, RelId qid)
+ CAst.make ~loc:!@loc @@ CTacPrj (e, RelId qid)
| e = SELF; ".("; qid = Prim.qualid; ")"; ":="; r = tac2expr LEVEL "5" ->
- Loc.tag ~loc:!@loc @@ CTacSet (e, RelId qid, r) ]
+ CAst.make ~loc:!@loc @@ CTacSet (e, RelId qid, r) ]
| "0"
[ "("; a = SELF; ")" -> a
| "("; a = SELF; ":"; t = tac2type; ")" ->
- Loc.tag ~loc:!@loc @@ CTacCnv (a, t)
+ CAst.make ~loc:!@loc @@ CTacCnv (a, t)
| "()" ->
- Loc.tag ~loc:!@loc @@ CTacCst (AbsKn (Tuple 0))
+ CAst.make ~loc:!@loc @@ CTacCst (AbsKn (Tuple 0))
| "("; ")" ->
- Loc.tag ~loc:!@loc @@ CTacCst (AbsKn (Tuple 0))
+ CAst.make ~loc:!@loc @@ CTacCst (AbsKn (Tuple 0))
| "["; a = LIST0 tac2expr LEVEL "5" SEP ";"; "]" ->
Tac2quote.of_list ~loc:!@loc (fun x -> x) a
| "{"; a = tac2rec_fieldexprs; "}" ->
- Loc.tag ~loc:!@loc @@ CTacRec a
+ CAst.make ~loc:!@loc @@ CTacRec a
| a = tactic_atom -> a ]
]
;
@@ -204,14 +204,14 @@ GEXTEND Gram
[ [ "'"; id = Prim.ident -> id ] ]
;
tactic_atom:
- [ [ n = Prim.integer -> Loc.tag ~loc:!@loc @@ CTacAtm (AtmInt n)
- | s = Prim.string -> Loc.tag ~loc:!@loc @@ CTacAtm (AtmStr s)
+ [ [ n = Prim.integer -> CAst.make ~loc:!@loc @@ CTacAtm (AtmInt n)
+ | s = Prim.string -> CAst.make ~loc:!@loc @@ CTacAtm (AtmStr s)
| id = Prim.qualid ->
- if Tac2env.is_constructor (snd id) then
- Loc.tag ~loc:!@loc @@ CTacCst (RelId id)
+ if Tac2env.is_constructor id.CAst.v then
+ CAst.make ~loc:!@loc @@ CTacCst (RelId id)
else
- Loc.tag ~loc:!@loc @@ CTacRef (RelId id)
- | "@"; id = Prim.ident -> Tac2quote.of_ident (Loc.tag ~loc:!@loc id)
+ CAst.make ~loc:!@loc @@ CTacRef (RelId id)
+ | "@"; id = Prim.ident -> Tac2quote.of_ident (CAst.make ~loc:!@loc id)
| "&"; id = lident -> Tac2quote.of_hyp ~loc:!@loc id
| "'"; c = Constr.constr -> inj_open_constr !@loc c
| IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> Tac2quote.of_constr c
@@ -227,7 +227,7 @@ GEXTEND Gram
let (pat, fn) = binder in
let te = match fn with
| None -> te
- | Some args -> Loc.tag ~loc:!@loc @@ CTacFun (args, te)
+ | Some args -> CAst.make ~loc:!@loc @@ CTacFun (args, te)
in
(pat, te)
] ]
@@ -235,42 +235,42 @@ GEXTEND Gram
let_binder:
[ [ pats = LIST1 input_fun ->
match pats with
- | [(_, CPatVar _) as pat] -> (pat, None)
- | ((_, CPatVar (Name id)) as pat) :: args -> (pat, Some args)
+ | [{CAst.v=CPatVar _} as pat] -> (pat, None)
+ | ({CAst.v=CPatVar (Name id)} as pat) :: args -> (pat, Some args)
| [pat] -> (pat, None)
| _ -> CErrors.user_err ~loc:!@loc (str "Invalid pattern")
] ]
;
tac2type:
[ "5" RIGHTA
- [ t1 = tac2type; "->"; t2 = tac2type -> Loc.tag ~loc:!@loc @@ CTypArrow (t1, t2) ]
+ [ t1 = tac2type; "->"; t2 = tac2type -> CAst.make ~loc:!@loc @@ CTypArrow (t1, t2) ]
| "2"
[ t = tac2type; "*"; tl = LIST1 tac2type LEVEL "1" SEP "*" ->
let tl = t :: tl in
- Loc.tag ~loc:!@loc @@ CTypRef (AbsKn (Tuple (List.length tl)), tl) ]
+ CAst.make ~loc:!@loc @@ CTypRef (AbsKn (Tuple (List.length tl)), tl) ]
| "1" LEFTA
- [ t = SELF; qid = Prim.qualid -> Loc.tag ~loc:!@loc @@ CTypRef (RelId qid, [t]) ]
+ [ t = SELF; qid = Prim.qualid -> CAst.make ~loc:!@loc @@ CTypRef (RelId qid, [t]) ]
| "0"
[ "("; t = tac2type LEVEL "5"; ")" -> t
- | id = typ_param -> Loc.tag ~loc:!@loc @@ CTypVar (Name id)
- | "_" -> Loc.tag ~loc:!@loc @@ CTypVar Anonymous
- | qid = Prim.qualid -> Loc.tag ~loc:!@loc @@ CTypRef (RelId qid, [])
+ | id = typ_param -> CAst.make ~loc:!@loc @@ CTypVar (Name id)
+ | "_" -> CAst.make ~loc:!@loc @@ CTypVar Anonymous
+ | qid = Prim.qualid -> CAst.make ~loc:!@loc @@ CTypRef (RelId qid, [])
| "("; p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = Prim.qualid ->
- Loc.tag ~loc:!@loc @@ CTypRef (RelId qid, p) ]
+ CAst.make ~loc:!@loc @@ CTypRef (RelId qid, p) ]
];
locident:
- [ [ id = Prim.ident -> Loc.tag ~loc:!@loc id ] ]
+ [ [ id = Prim.ident -> CAst.make ~loc:!@loc id ] ]
;
binder:
- [ [ "_" -> Loc.tag ~loc:!@loc Anonymous
- | l = Prim.ident -> Loc.tag ~loc:!@loc (Name l) ] ]
+ [ [ "_" -> CAst.make ~loc:!@loc Anonymous
+ | l = Prim.ident -> CAst.make ~loc:!@loc (Name l) ] ]
;
input_fun:
[ [ b = tac2pat LEVEL "0" -> b ] ]
;
tac2def_body:
[ [ name = binder; it = LIST0 input_fun; ":="; e = tac2expr ->
- let e = if List.is_empty it then e else Loc.tag ~loc:!@loc @@ CTacFun (it, e) in
+ let e = if List.is_empty it then e else CAst.make ~loc:!@loc @@ CTacFun (it, e) in
(name, e)
] ]
;
@@ -319,8 +319,8 @@ GEXTEND Gram
;
tac2typ_prm:
[ [ -> []
- | id = typ_param -> [Loc.tag ~loc:!@loc id]
- | "("; ids = LIST1 [ id = typ_param -> Loc.tag ~loc:!@loc id ] SEP "," ;")" -> ids
+ | id = typ_param -> [CAst.make ~loc:!@loc id]
+ | "("; ids = LIST1 [ id = typ_param -> CAst.make ~loc:!@loc id ] SEP "," ;")" -> ids
] ]
;
tac2typ_def:
@@ -345,13 +345,13 @@ GEXTEND Gram
] ]
;
syn_node:
- [ [ "_" -> Loc.tag ~loc:!@loc None
- | id = Prim.ident -> Loc.tag ~loc:!@loc (Some id)
+ [ [ "_" -> CAst.make ~loc:!@loc None
+ | id = Prim.ident -> CAst.make ~loc:!@loc (Some id)
] ]
;
sexpr:
- [ [ s = Prim.string -> SexprStr (Loc.tag ~loc:!@loc s)
- | n = Prim.integer -> SexprInt (Loc.tag ~loc:!@loc n)
+ [ [ s = Prim.string -> SexprStr (CAst.make ~loc:!@loc s)
+ | n = Prim.integer -> SexprInt (CAst.make ~loc:!@loc n)
| id = syn_node -> SexprRec (!@loc, id, [])
| id = syn_node; "("; tok = LIST1 sexpr SEP "," ; ")" ->
SexprRec (!@loc, id, tok)
@@ -369,11 +369,11 @@ GEXTEND Gram
] ]
;
lident:
- [ [ id = Prim.ident -> Loc.tag ~loc:!@loc id ] ]
+ [ [ id = Prim.ident -> CAst.make ~loc:!@loc id ] ]
;
globref:
[ [ "&"; id = Prim.ident -> Libnames.Ident (Loc.tag ~loc:!@loc id)
- | qid = Prim.qualid -> Libnames.Qualid qid
+ | qid = Prim.qualid -> Libnames.Qualid (Loc.tag ~loc:!@loc qid.CAst.v)
] ]
;
END
@@ -390,38 +390,38 @@ GEXTEND Gram
q_destruction_arg q_reference q_with_bindings q_constr_matching
q_goal_matching q_hintdb q_move_location q_pose q_assert;
anti:
- [ [ "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id) ] ]
+ [ [ "$"; id = Prim.ident -> QAnti (CAst.make ~loc:!@loc id) ] ]
;
ident_or_anti:
[ [ id = lident -> QExpr id
- | "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id)
+ | "$"; id = Prim.ident -> QAnti (CAst.make ~loc:!@loc id)
] ]
;
lident:
- [ [ id = Prim.ident -> Loc.tag ~loc:!@loc id ] ]
+ [ [ id = Prim.ident -> CAst.make ~loc:!@loc id ] ]
;
lnatural:
- [ [ n = Prim.natural -> Loc.tag ~loc:!@loc n ] ]
+ [ [ n = Prim.natural -> CAst.make ~loc:!@loc n ] ]
;
q_ident:
[ [ id = ident_or_anti -> id ] ]
;
qhyp:
[ [ x = anti -> x
- | n = lnatural -> QExpr (Loc.tag ~loc:!@loc @@ QAnonHyp n)
- | id = lident -> QExpr (Loc.tag ~loc:!@loc @@ QNamedHyp id)
+ | n = lnatural -> QExpr (CAst.make ~loc:!@loc @@ QAnonHyp n)
+ | id = lident -> QExpr (CAst.make ~loc:!@loc @@ QNamedHyp id)
] ]
;
simple_binding:
[ [ "("; h = qhyp; ":="; c = Constr.lconstr; ")" ->
- Loc.tag ~loc:!@loc (h, c)
+ CAst.make ~loc:!@loc (h, c)
] ]
;
bindings:
[ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding ->
- Loc.tag ~loc:!@loc @@ QExplicitBindings bl
+ CAst.make ~loc:!@loc @@ QExplicitBindings bl
| bl = LIST1 Constr.constr ->
- Loc.tag ~loc:!@loc @@ QImplicitBindings bl
+ CAst.make ~loc:!@loc @@ QImplicitBindings bl
] ]
;
q_bindings:
@@ -431,53 +431,53 @@ GEXTEND Gram
[ [ bl = with_bindings -> bl ] ]
;
intropatterns:
- [ [ l = LIST0 nonsimple_intropattern -> Loc.tag ~loc:!@loc l ]]
+ [ [ l = LIST0 nonsimple_intropattern -> CAst.make ~loc:!@loc l ]]
;
(* ne_intropatterns: *)
(* [ [ l = LIST1 nonsimple_intropattern -> l ]] *)
(* ; *)
or_and_intropattern:
- [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> Loc.tag ~loc:!@loc @@ QIntroOrPattern tc
- | "()" -> Loc.tag ~loc:!@loc @@ QIntroAndPattern (Loc.tag ~loc:!@loc [])
- | "("; si = simple_intropattern; ")" -> Loc.tag ~loc:!@loc @@ QIntroAndPattern (Loc.tag ~loc:!@loc [si])
+ [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> CAst.make ~loc:!@loc @@ QIntroOrPattern tc
+ | "()" -> CAst.make ~loc:!@loc @@ QIntroAndPattern (CAst.make ~loc:!@loc [])
+ | "("; si = simple_intropattern; ")" -> CAst.make ~loc:!@loc @@ QIntroAndPattern (CAst.make ~loc:!@loc [si])
| "("; si = simple_intropattern; ",";
tc = LIST1 simple_intropattern SEP "," ; ")" ->
- Loc.tag ~loc:!@loc @@ QIntroAndPattern (Loc.tag ~loc:!@loc (si::tc))
+ CAst.make ~loc:!@loc @@ QIntroAndPattern (CAst.make ~loc:!@loc (si::tc))
| "("; si = simple_intropattern; "&";
tc = LIST1 simple_intropattern SEP "&" ; ")" ->
(* (A & B & C) is translated into (A,(B,C)) *)
let rec pairify = function
- | ([]|[_]|[_;_]) as l -> Loc.tag ~loc:!@loc l
+ | ([]|[_]|[_;_]) as l -> CAst.make ~loc:!@loc l
| t::q ->
let q =
- Loc.tag ~loc:!@loc @@
- QIntroAction (Loc.tag ~loc:!@loc @@
- QIntroOrAndPattern (Loc.tag ~loc:!@loc @@
+ CAst.make ~loc:!@loc @@
+ QIntroAction (CAst.make ~loc:!@loc @@
+ QIntroOrAndPattern (CAst.make ~loc:!@loc @@
QIntroAndPattern (pairify q)))
in
- Loc.tag ~loc:!@loc [t; q]
- in Loc.tag ~loc:!@loc @@ QIntroAndPattern (pairify (si::tc)) ] ]
+ CAst.make ~loc:!@loc [t; q]
+ in CAst.make ~loc:!@loc @@ QIntroAndPattern (pairify (si::tc)) ] ]
;
equality_intropattern:
- [ [ "->" -> Loc.tag ~loc:!@loc @@ QIntroRewrite true
- | "<-" -> Loc.tag ~loc:!@loc @@ QIntroRewrite false
- | "[="; tc = intropatterns; "]" -> Loc.tag ~loc:!@loc @@ QIntroInjection tc ] ]
+ [ [ "->" -> CAst.make ~loc:!@loc @@ QIntroRewrite true
+ | "<-" -> CAst.make ~loc:!@loc @@ QIntroRewrite false
+ | "[="; tc = intropatterns; "]" -> CAst.make ~loc:!@loc @@ QIntroInjection tc ] ]
;
naming_intropattern:
[ [ LEFTQMARK; id = lident ->
- Loc.tag ~loc:!@loc @@ QIntroFresh (QExpr id)
+ CAst.make ~loc:!@loc @@ QIntroFresh (QExpr id)
| "?$"; id = lident ->
- Loc.tag ~loc:!@loc @@ QIntroFresh (QAnti id)
+ CAst.make ~loc:!@loc @@ QIntroFresh (QAnti id)
| "?" ->
- Loc.tag ~loc:!@loc @@ QIntroAnonymous
+ CAst.make ~loc:!@loc @@ QIntroAnonymous
| id = ident_or_anti ->
- Loc.tag ~loc:!@loc @@ QIntroIdentifier id
+ CAst.make ~loc:!@loc @@ QIntroIdentifier id
] ]
;
nonsimple_intropattern:
[ [ l = simple_intropattern -> l
- | "*" -> Loc.tag ~loc:!@loc @@ QIntroForthcoming true
- | "**" -> Loc.tag ~loc:!@loc @@ QIntroForthcoming false ]]
+ | "*" -> CAst.make ~loc:!@loc @@ QIntroForthcoming true
+ | "**" -> CAst.make ~loc:!@loc @@ QIntroForthcoming false ]]
;
simple_intropattern:
[ [ pat = simple_intropattern_closed ->
@@ -488,13 +488,13 @@ GEXTEND Gram
;
simple_intropattern_closed:
[ [ pat = or_and_intropattern ->
- Loc.tag ~loc:!@loc @@ QIntroAction (Loc.tag ~loc:!@loc @@ QIntroOrAndPattern pat)
+ CAst.make ~loc:!@loc @@ QIntroAction (CAst.make ~loc:!@loc @@ QIntroOrAndPattern pat)
| pat = equality_intropattern ->
- Loc.tag ~loc:!@loc @@ QIntroAction pat
+ CAst.make ~loc:!@loc @@ QIntroAction pat
| "_" ->
- Loc.tag ~loc:!@loc @@ QIntroAction (Loc.tag ~loc:!@loc @@ QIntroWildcard)
+ CAst.make ~loc:!@loc @@ QIntroAction (CAst.make ~loc:!@loc @@ QIntroWildcard)
| pat = naming_intropattern ->
- Loc.tag ~loc:!@loc @@ QIntroNaming pat
+ CAst.make ~loc:!@loc @@ QIntroNaming pat
] ]
;
q_intropatterns:
@@ -505,7 +505,7 @@ GEXTEND Gram
;
nat_or_anti:
[ [ n = lnatural -> QExpr n
- | "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id)
+ | "$"; id = Prim.ident -> QAnti (CAst.make ~loc:!@loc id)
] ]
;
eqn_ipat:
@@ -514,15 +514,15 @@ GEXTEND Gram
] ]
;
with_bindings:
- [ [ "with"; bl = bindings -> bl | -> Loc.tag ~loc:!@loc @@ QNoBindings ] ]
+ [ [ "with"; bl = bindings -> bl | -> CAst.make ~loc:!@loc @@ QNoBindings ] ]
;
constr_with_bindings:
- [ [ c = Constr.constr; l = with_bindings -> Loc.tag ~loc:!@loc @@ (c, l) ] ]
+ [ [ c = Constr.constr; l = with_bindings -> CAst.make ~loc:!@loc @@ (c, l) ] ]
;
destruction_arg:
- [ [ n = lnatural -> Loc.tag ~loc:!@loc @@ QElimOnAnonHyp n
- | id = lident -> Loc.tag ~loc:!@loc @@ QElimOnIdent id
- | c = constr_with_bindings -> Loc.tag ~loc:!@loc @@ QElimOnConstr c
+ [ [ n = lnatural -> CAst.make ~loc:!@loc @@ QElimOnAnonHyp n
+ | id = lident -> CAst.make ~loc:!@loc @@ QElimOnIdent id
+ | c = constr_with_bindings -> CAst.make ~loc:!@loc @@ QElimOnConstr c
] ]
;
q_destruction_arg:
@@ -534,13 +534,13 @@ GEXTEND Gram
] ]
;
occs_nums:
- [ [ nl = LIST1 nat_or_anti -> Loc.tag ~loc:!@loc @@ QOnlyOccurrences nl
+ [ [ nl = LIST1 nat_or_anti -> CAst.make ~loc:!@loc @@ QOnlyOccurrences nl
| "-"; n = nat_or_anti; nl = LIST0 nat_or_anti ->
- Loc.tag ~loc:!@loc @@ QAllOccurrencesBut (n::nl)
+ CAst.make ~loc:!@loc @@ QAllOccurrencesBut (n::nl)
] ]
;
occs:
- [ [ "at"; occs = occs_nums -> occs | -> Loc.tag ~loc:!@loc QAllOccurrences ] ]
+ [ [ "at"; occs = occs_nums -> occs | -> CAst.make ~loc:!@loc QAllOccurrences ] ]
;
hypident:
[ [ id = ident_or_anti ->
@@ -562,13 +562,13 @@ GEXTEND Gram
| hl = LIST0 hypident_occ SEP ","; "|-"; occs = concl_occ ->
{ q_onhyps = Some hl; q_concl_occs = occs }
| hl = LIST0 hypident_occ SEP "," ->
- { q_onhyps = Some hl; q_concl_occs = Loc.tag ~loc:!@loc QNoOccurrences }
+ { q_onhyps = Some hl; q_concl_occs = CAst.make ~loc:!@loc QNoOccurrences }
] ]
;
clause:
- [ [ "in"; cl = in_clause -> Loc.tag ~loc:!@loc @@ cl
+ [ [ "in"; cl = in_clause -> CAst.make ~loc:!@loc @@ cl
| "at"; occs = occs_nums ->
- Loc.tag ~loc:!@loc @@ { q_onhyps = Some []; q_concl_occs = occs }
+ CAst.make ~loc:!@loc @@ { q_onhyps = Some []; q_concl_occs = occs }
] ]
;
q_clause:
@@ -576,13 +576,13 @@ GEXTEND Gram
;
concl_occ:
[ [ "*"; occs = occs -> occs
- | -> Loc.tag ~loc:!@loc QNoOccurrences
+ | -> CAst.make ~loc:!@loc QNoOccurrences
] ]
;
induction_clause:
[ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat;
cl = OPT clause ->
- Loc.tag ~loc:!@loc @@ {
+ CAst.make ~loc:!@loc @@ {
indcl_arg = c;
indcl_eqn = eq;
indcl_as = pat;
@@ -595,38 +595,38 @@ GEXTEND Gram
;
conversion:
[ [ c = Constr.constr ->
- Loc.tag ~loc:!@loc @@ QConvert c
+ CAst.make ~loc:!@loc @@ QConvert c
| c1 = Constr.constr; "with"; c2 = Constr.constr ->
- Loc.tag ~loc:!@loc @@ QConvertWith (c1, c2)
+ CAst.make ~loc:!@loc @@ QConvertWith (c1, c2)
] ]
;
q_conversion:
[ [ c = conversion -> c ] ]
;
orient:
- [ [ "->" -> Loc.tag ~loc:!@loc (Some true)
- | "<-" -> Loc.tag ~loc:!@loc (Some false)
- | -> Loc.tag ~loc:!@loc None
+ [ [ "->" -> CAst.make ~loc:!@loc (Some true)
+ | "<-" -> CAst.make ~loc:!@loc (Some false)
+ | -> CAst.make ~loc:!@loc None
]]
;
rewriter:
[ [ "!"; c = constr_with_bindings ->
- (Loc.tag ~loc:!@loc @@ QRepeatPlus,c)
+ (CAst.make ~loc:!@loc @@ QRepeatPlus,c)
| ["?"| LEFTQMARK]; c = constr_with_bindings ->
- (Loc.tag ~loc:!@loc @@ QRepeatStar,c)
+ (CAst.make ~loc:!@loc @@ QRepeatStar,c)
| n = lnatural; "!"; c = constr_with_bindings ->
- (Loc.tag ~loc:!@loc @@ QPrecisely n,c)
+ (CAst.make ~loc:!@loc @@ QPrecisely n,c)
| n = lnatural; ["?" | LEFTQMARK]; c = constr_with_bindings ->
- (Loc.tag ~loc:!@loc @@ QUpTo n,c)
+ (CAst.make ~loc:!@loc @@ QUpTo n,c)
| n = lnatural; c = constr_with_bindings ->
- (Loc.tag ~loc:!@loc @@ QPrecisely n,c)
+ (CAst.make ~loc:!@loc @@ QPrecisely n,c)
| c = constr_with_bindings ->
- (Loc.tag ~loc:!@loc @@ QPrecisely (Loc.tag 1), c)
+ (CAst.make ~loc:!@loc @@ QPrecisely (CAst.make 1), c)
] ]
;
oriented_rewriter:
[ [ b = orient; (m, c) = rewriter ->
- Loc.tag ~loc:!@loc @@ {
+ CAst.make ~loc:!@loc @@ {
rew_orient = b;
rew_repeat = m;
rew_equatn = c;
@@ -651,52 +651,52 @@ GEXTEND Gram
] ]
;
q_dispatch:
- [ [ d = tactic_then_gen -> Loc.tag ~loc:!@loc d ] ]
+ [ [ d = tactic_then_gen -> CAst.make ~loc:!@loc d ] ]
;
q_occurrences:
[ [ occs = occs -> occs ] ]
;
red_flag:
- [ [ IDENT "beta" -> Loc.tag ~loc:!@loc @@ QBeta
- | IDENT "iota" -> Loc.tag ~loc:!@loc @@ QIota
- | IDENT "match" -> Loc.tag ~loc:!@loc @@ QMatch
- | IDENT "fix" -> Loc.tag ~loc:!@loc @@ QFix
- | IDENT "cofix" -> Loc.tag ~loc:!@loc @@ QCofix
- | IDENT "zeta" -> Loc.tag ~loc:!@loc @@ QZeta
+ [ [ IDENT "beta" -> CAst.make ~loc:!@loc @@ QBeta
+ | IDENT "iota" -> CAst.make ~loc:!@loc @@ QIota
+ | IDENT "match" -> CAst.make ~loc:!@loc @@ QMatch
+ | IDENT "fix" -> CAst.make ~loc:!@loc @@ QFix
+ | IDENT "cofix" -> CAst.make ~loc:!@loc @@ QCofix
+ | IDENT "zeta" -> CAst.make ~loc:!@loc @@ QZeta
| IDENT "delta"; d = delta_flag -> d
] ]
;
refglobal:
[ [ "&"; id = Prim.ident -> QExpr (Libnames.Ident (Loc.tag ~loc:!@loc id))
- | qid = Prim.qualid -> QExpr (Libnames.Qualid qid)
- | "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id)
+ | qid = Prim.qualid -> QExpr (Libnames.Qualid Loc.(tag ~loc:!@loc qid.CAst.v))
+ | "$"; id = Prim.ident -> QAnti (CAst.make ~loc:!@loc id)
] ]
;
q_reference:
[ [ r = refglobal -> r ] ]
;
refglobals:
- [ [ gl = LIST1 refglobal -> Loc.tag ~loc:!@loc gl ] ]
+ [ [ gl = LIST1 refglobal -> CAst.make ~loc:!@loc gl ] ]
;
delta_flag:
- [ [ "-"; "["; idl = refglobals; "]" -> Loc.tag ~loc:!@loc @@ QDeltaBut idl
- | "["; idl = refglobals; "]" -> Loc.tag ~loc:!@loc @@ QConst idl
- | -> Loc.tag ~loc:!@loc @@ QDeltaBut (Loc.tag ~loc:!@loc [])
+ [ [ "-"; "["; idl = refglobals; "]" -> CAst.make ~loc:!@loc @@ QDeltaBut idl
+ | "["; idl = refglobals; "]" -> CAst.make ~loc:!@loc @@ QConst idl
+ | -> CAst.make ~loc:!@loc @@ QDeltaBut (CAst.make ~loc:!@loc [])
] ]
;
strategy_flag:
- [ [ s = LIST1 red_flag -> Loc.tag ~loc:!@loc s
+ [ [ s = LIST1 red_flag -> CAst.make ~loc:!@loc s
| d = delta_flag ->
- Loc.tag ~loc:!@loc
- [Loc.tag ~loc:!@loc QBeta; Loc.tag ~loc:!@loc QIota; Loc.tag ~loc:!@loc QZeta; d]
+ CAst.make ~loc:!@loc
+ [CAst.make ~loc:!@loc QBeta; CAst.make ~loc:!@loc QIota; CAst.make ~loc:!@loc QZeta; d]
] ]
;
q_strategy_flag:
[ [ flag = strategy_flag -> flag ] ]
;
hintdb:
- [ [ "*" -> Loc.tag ~loc:!@loc @@ QHintAll
- | l = LIST1 ident_or_anti -> Loc.tag ~loc:!@loc @@ QHintDbs l
+ [ [ "*" -> CAst.make ~loc:!@loc @@ QHintAll
+ | l = LIST1 ident_or_anti -> CAst.make ~loc:!@loc @@ QHintDbs l
] ]
;
q_hintdb:
@@ -704,17 +704,17 @@ GEXTEND Gram
;
match_pattern:
[ [ IDENT "context"; id = OPT Prim.ident;
- "["; pat = Constr.lconstr_pattern; "]" -> Loc.tag ~loc:!@loc @@ QConstrMatchContext (id, pat)
- | pat = Constr.lconstr_pattern -> Loc.tag ~loc:!@loc @@ QConstrMatchPattern pat ] ]
+ "["; pat = Constr.lconstr_pattern; "]" -> CAst.make ~loc:!@loc @@ QConstrMatchContext (id, pat)
+ | pat = Constr.lconstr_pattern -> CAst.make ~loc:!@loc @@ QConstrMatchPattern pat ] ]
;
match_rule:
[ [ mp = match_pattern; "=>"; tac = tac2expr ->
- Loc.tag ~loc:!@loc @@ (mp, tac)
+ CAst.make ~loc:!@loc @@ (mp, tac)
] ]
;
match_list:
- [ [ mrl = LIST1 match_rule SEP "|" -> Loc.tag ~loc:!@loc @@ mrl
- | "|"; mrl = LIST1 match_rule SEP "|" -> Loc.tag ~loc:!@loc @@ mrl ] ]
+ [ [ mrl = LIST1 match_rule SEP "|" -> CAst.make ~loc:!@loc @@ mrl
+ | "|"; mrl = LIST1 match_rule SEP "|" -> CAst.make ~loc:!@loc @@ mrl ] ]
;
q_constr_matching:
[ [ m = match_list -> m ] ]
@@ -724,7 +724,7 @@ GEXTEND Gram
;
gmatch_pattern:
[ [ "["; hl = LIST0 gmatch_hyp_pattern SEP ","; "|-"; p = match_pattern; "]" ->
- Loc.tag ~loc:!@loc @@ {
+ CAst.make ~loc:!@loc @@ {
q_goal_match_concl = p;
q_goal_match_hyps = hl;
}
@@ -732,21 +732,21 @@ GEXTEND Gram
;
gmatch_rule:
[ [ mp = gmatch_pattern; "=>"; tac = tac2expr ->
- Loc.tag ~loc:!@loc @@ (mp, tac)
+ CAst.make ~loc:!@loc @@ (mp, tac)
] ]
;
gmatch_list:
- [ [ mrl = LIST1 gmatch_rule SEP "|" -> Loc.tag ~loc:!@loc @@ mrl
- | "|"; mrl = LIST1 gmatch_rule SEP "|" -> Loc.tag ~loc:!@loc @@ mrl ] ]
+ [ [ mrl = LIST1 gmatch_rule SEP "|" -> CAst.make ~loc:!@loc @@ mrl
+ | "|"; mrl = LIST1 gmatch_rule SEP "|" -> CAst.make ~loc:!@loc @@ mrl ] ]
;
q_goal_matching:
[ [ m = gmatch_list -> m ] ]
;
move_location:
- [ [ "at"; IDENT "top" -> Loc.tag ~loc:!@loc @@ QMoveFirst
- | "at"; IDENT "bottom" -> Loc.tag ~loc:!@loc @@ QMoveLast
- | IDENT "after"; id = ident_or_anti -> Loc.tag ~loc:!@loc @@ QMoveAfter id
- | IDENT "before"; id = ident_or_anti -> Loc.tag ~loc:!@loc @@ QMoveBefore id
+ [ [ "at"; IDENT "top" -> CAst.make ~loc:!@loc @@ QMoveFirst
+ | "at"; IDENT "bottom" -> CAst.make ~loc:!@loc @@ QMoveLast
+ | IDENT "after"; id = ident_or_anti -> CAst.make ~loc:!@loc @@ QMoveAfter id
+ | IDENT "before"; id = ident_or_anti -> CAst.make ~loc:!@loc @@ QMoveBefore id
] ]
;
q_move_location:
@@ -759,8 +759,8 @@ GEXTEND Gram
;
pose:
[ [ test_lpar_id_coloneq; "("; id = ident_or_anti; ":="; c = Constr.lconstr; ")" ->
- Loc.tag ~loc:!@loc (Some id, c)
- | c = Constr.constr; na = as_name -> Loc.tag ~loc:!@loc (na, c)
+ CAst.make ~loc:!@loc (Some id, c)
+ | c = Constr.constr; na = as_name -> CAst.make ~loc:!@loc (na, c)
] ]
;
q_pose:
@@ -778,13 +778,13 @@ GEXTEND Gram
;
assertion:
[ [ test_lpar_id_coloneq; "("; id = ident_or_anti; ":="; c = Constr.lconstr; ")" ->
- Loc.tag ~loc:!@loc (QAssertValue (id, c))
+ CAst.make ~loc:!@loc (QAssertValue (id, c))
| test_lpar_id_colon; "("; id = ident_or_anti; ":"; c = Constr.lconstr; ")"; tac = by_tactic ->
let loc = !@loc in
- let ipat = Loc.tag ~loc @@ QIntroNaming (Loc.tag ~loc @@ QIntroIdentifier id) in
- Loc.tag ~loc (QAssertType (Some ipat, c, tac))
+ let ipat = CAst.make ~loc @@ QIntroNaming (CAst.make ~loc @@ QIntroIdentifier id) in
+ CAst.make ~loc (QAssertType (Some ipat, c, tac))
| c = Constr.constr; ipat = as_ipat; tac = by_tactic ->
- Loc.tag ~loc:!@loc (QAssertType (ipat, c, tac))
+ CAst.make ~loc:!@loc (QAssertType (ipat, c, tac))
] ]
;
q_assert:
@@ -801,7 +801,7 @@ GEXTEND Gram
let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
CAst.make ~loc:!@loc (CHole (None, IntroAnonymous, Some arg))
| test_ampersand_ident; "&"; id = Prim.ident ->
- let tac = Tac2quote.of_exact_hyp ~loc:!@loc (Loc.tag ~loc:!@loc id) in
+ let tac = Tac2quote.of_exact_hyp ~loc:!@loc (CAst.make ~loc:!@loc id) in
let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
CAst.make ~loc:!@loc (CHole (None, IntroAnonymous, Some arg))
| test_dollar_ident; "$"; id = Prim.ident ->
diff --git a/src/tac2core.ml b/src/tac2core.ml
index c16e72b801..c6c3f26b6b 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -516,7 +516,7 @@ let () = define3 "constr_in_context" ident constr closure begin fun id t c ->
Proofview.Unsafe.tclEVARS sigma >>= fun () ->
Proofview.Unsafe.tclSETGOALS [Proofview.with_empty_state evk] >>= fun () ->
thaw c >>= fun _ ->
- Proofview.Unsafe.tclSETGOALS [Proofview.with_empty_state (Proofview.Goal.goal (Proofview.Goal.assume gl))] >>= fun () ->
+ Proofview.Unsafe.tclSETGOALS [Proofview.with_empty_state (Proofview.Goal.goal gl)] >>= fun () ->
let args = List.map (fun d -> EConstr.mkVar (get_id d)) (EConstr.named_context env) in
let args = Array.of_list (EConstr.mkRel 1 :: args) in
let ans = EConstr.mkEvar (evk, args) in
@@ -744,7 +744,6 @@ end
let () = define1 "refine" closure begin fun c ->
let c = thaw c >>= fun c -> Proofview.tclUNIT ((), Value.to_constr c) in
Proofview.Goal.enter begin fun gl ->
- let gl = Proofview.Goal.assume gl in
Refine.generic_refine ~typecheck:true c gl
end >>= fun () -> return v_unit
end
@@ -1023,10 +1022,10 @@ let () =
let add_scope s f =
Tac2entries.register_scope (Id.of_string s) f
-let rec pr_scope = function
-| SexprStr (_, s) -> qstring s
-| SexprInt (_, n) -> Pp.int n
-| SexprRec (_, (_, na), args) ->
+let rec pr_scope = let open CAst in function
+| SexprStr {v=s} -> qstring s
+| SexprInt {v=n} -> Pp.int n
+| SexprRec (_, {v=na}, args) ->
let na = match na with
| None -> str "_"
| Some id -> Id.print id
@@ -1037,27 +1036,29 @@ let scope_fail s args =
let args = str "(" ++ prlist_with_sep (fun () -> str ", ") pr_scope args ++ str ")" in
CErrors.user_err (str "Invalid arguments " ++ args ++ str " in scope " ++ str s)
-let q_unit = Loc.tag @@ CTacCst (AbsKn (Tuple 0))
+let q_unit = CAst.make @@ CTacCst (AbsKn (Tuple 0))
let add_generic_scope s entry arg =
let parse = function
| [] ->
let scope = Extend.Aentry entry in
- let act x = Loc.tag @@ CTacExt (arg, x) in
+ let act x = CAst.make @@ CTacExt (arg, x) in
Tac2entries.ScopeRule (scope, act)
| arg -> scope_fail s arg
in
add_scope s parse
+open CAst
+
let () = add_scope "keyword" begin function
-| [SexprStr (loc, s)] ->
+| [SexprStr {loc;v=s}] ->
let scope = Extend.Atoken (Tok.KEYWORD s) in
Tac2entries.ScopeRule (scope, (fun _ -> q_unit))
| arg -> scope_fail "keyword" arg
end
let () = add_scope "terminal" begin function
-| [SexprStr (loc, s)] ->
+| [SexprStr {loc;v=s}] ->
let scope = Extend.Atoken (CLexer.terminal s) in
Tac2entries.ScopeRule (scope, (fun _ -> q_unit))
| arg -> scope_fail "terminal" arg
@@ -1069,7 +1070,7 @@ let () = add_scope "list0" begin function
let scope = Extend.Alist0 scope in
let act l = Tac2quote.of_list act l in
Tac2entries.ScopeRule (scope, act)
-| [tok; SexprStr (_, str)] ->
+| [tok; SexprStr {v=str}] ->
let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
let sep = Extend.Atoken (CLexer.terminal str) in
let scope = Extend.Alist0sep (scope, sep) in
@@ -1084,7 +1085,7 @@ let () = add_scope "list1" begin function
let scope = Extend.Alist1 scope in
let act l = Tac2quote.of_list act l in
Tac2entries.ScopeRule (scope, act)
-| [tok; SexprStr (_, str)] ->
+| [tok; SexprStr {v=str}] ->
let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
let sep = Extend.Atoken (CLexer.terminal str) in
let scope = Extend.Alist1sep (scope, sep) in
@@ -1099,9 +1100,9 @@ let () = add_scope "opt" begin function
let scope = Extend.Aopt scope in
let act opt = match opt with
| None ->
- Loc.tag @@ CTacCst (AbsKn (Other Core.c_none))
+ CAst.make @@ CTacCst (AbsKn (Other Core.c_none))
| Some x ->
- Loc.tag @@ CTacApp (Loc.tag @@ CTacCst (AbsKn (Other Core.c_some)), [act x])
+ CAst.make @@ CTacApp (CAst.make @@ CTacCst (AbsKn (Other Core.c_some)), [act x])
in
Tac2entries.ScopeRule (scope, act)
| arg -> scope_fail "opt" arg
@@ -1129,7 +1130,7 @@ let () = add_scope "tactic" begin function
let scope = Extend.Aentryl (tac2expr, 5) in
let act tac = tac in
Tac2entries.ScopeRule (scope, act)
-| [SexprInt (loc, n)] as arg ->
+| [SexprInt {loc;v=n}] as arg ->
let () = if n < 0 || n > 6 then scope_fail "tactic" arg in
let scope = Extend.Aentryl (tac2expr, n) in
let act tac = tac in
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 1631880c71..e4bddf439b 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -8,6 +8,7 @@
open Pp
open Util
+open CAst
open CErrors
open Names
open Libnames
@@ -277,62 +278,61 @@ let fresh_var avoid x =
in
Namegen.next_ident_away_from (Id.of_string x) bad
-let extract_pattern_type (loc, p as pat) = match p with
+let extract_pattern_type ({loc;v=p} as pat) = match p with
| CPatCnv (pat, ty) -> pat, Some ty
| CPatVar _ | CPatRef _ -> pat, None
(** Mangle recursive tactics *)
let inline_rec_tactic tactics =
- let avoid = List.fold_left (fun accu ((_, id), _) -> Id.Set.add id accu) Id.Set.empty tactics in
- let map (id, e) = match snd e with
+ let avoid = List.fold_left (fun accu ({v=id}, _) -> Id.Set.add id accu) Id.Set.empty tactics in
+ let map (id, e) = match e.v with
| CTacFun (pat, _) -> (id, List.map extract_pattern_type pat, e)
| _ ->
- let loc, _ = id in
- user_err ?loc (str "Recursive tactic definitions must be functions")
+ user_err ?loc:id.loc (str "Recursive tactic definitions must be functions")
in
let tactics = List.map map tactics in
let map (id, pat, e) =
let fold_var (avoid, ans) (pat, _) =
let id = fresh_var avoid "x" in
- let loc = loc_of_patexpr pat in
- (Id.Set.add id avoid, Loc.tag ?loc id :: ans)
+ let loc = pat.loc in
+ (Id.Set.add id avoid, CAst.make ?loc id :: ans)
in
(** Fresh variables to abstract over the function patterns *)
let _, vars = List.fold_left fold_var (avoid, []) pat in
- let map_body ((loc, id), _, e) = (Loc.tag ?loc @@ CPatVar (Name id)), e in
+ let map_body ({loc;v=id}, _, e) = CAst.(make ?loc @@ CPatVar (Name id)), e in
let bnd = List.map map_body tactics in
- let pat_of_id (loc, id) = (Loc.tag ?loc @@ CPatVar (Name id)) in
- let var_of_id (loc, id) =
- let qid = (loc, qualid_of_ident id) in
- Loc.tag ?loc @@ CTacRef (RelId qid)
+ let pat_of_id {loc;v=id} = CAst.make ?loc @@ CPatVar (Name id) in
+ let var_of_id {loc;v=id} =
+ let qid = CAst.make ?loc @@ qualid_of_ident id in
+ CAst.make ?loc @@ CTacRef (RelId qid)
in
- let loc0 = loc_of_tacexpr e in
+ let loc0 = e.loc in
let vpat = List.map pat_of_id vars in
let varg = List.map var_of_id vars in
- let e = Loc.tag ?loc:loc0 @@ CTacLet (true, bnd, Loc.tag ?loc:loc0 @@ CTacApp (var_of_id id, varg)) in
- (id, Loc.tag ?loc:loc0 @@ CTacFun (vpat, e))
+ let e = CAst.make ?loc:loc0 @@ CTacLet (true, bnd, CAst.make ?loc:loc0 @@ CTacApp (var_of_id id, varg)) in
+ (id, CAst.make ?loc:loc0 @@ CTacFun (vpat, e))
in
List.map map tactics
-let check_lowercase (loc, id) =
+let check_lowercase {loc;v=id} =
if Tac2env.is_constructor (Libnames.qualid_of_ident id) then
user_err ?loc (str "The identifier " ++ Id.print id ++ str " must be lowercase")
let register_ltac ?(local = false) ?(mut = false) isrec tactics =
- let map ((loc, na), e) =
+ let map ({loc;v=na}, e) =
let id = match na with
| Anonymous ->
user_err ?loc (str "Tactic definition must have a name")
| Name id -> id
in
- let () = check_lowercase (loc, id) in
- ((loc, id), e)
+ let () = check_lowercase CAst.(make ?loc id) in
+ (CAst.(make ?loc id), e)
in
let tactics = List.map map tactics in
let tactics =
if isrec then inline_rec_tactic tactics else tactics
in
- let map ((loc, id), e) =
+ let map ({loc;v=id}, e) =
let (e, t) = intern ~strict:true e in
let () =
if not (is_value e) then
@@ -360,23 +360,23 @@ let register_ltac ?(local = false) ?(mut = false) isrec tactics =
in
List.iter iter defs
-let qualid_to_ident (loc, qid) =
+let qualid_to_ident {loc;v=qid} =
let (dp, id) = Libnames.repr_qualid qid in
- if DirPath.is_empty dp then (loc, id)
+ if DirPath.is_empty dp then CAst.make ?loc id
else user_err ?loc (str "Identifier expected")
let register_typedef ?(local = false) isrec types =
- let same_name ((_, id1), _) ((_, id2), _) = Id.equal id1 id2 in
+ let same_name ({v=id1}, _) ({v=id2}, _) = Id.equal id1 id2 in
let () = match List.duplicates same_name types with
| [] -> ()
- | ((loc, id), _) :: _ ->
+ | ({loc;v=id}, _) :: _ ->
user_err ?loc (str "Multiple definition of the type name " ++ Id.print id)
in
- let check ((loc, id), (params, def)) =
- let same_name (_, id1) (_, id2) = Id.equal id1 id2 in
+ let check ({loc;v=id}, (params, def)) =
+ let same_name {v=id1} {v=id2} = Id.equal id1 id2 in
let () = match List.duplicates same_name params with
| [] -> ()
- | (loc, id) :: _ ->
+ | {loc;v=id} :: _ ->
user_err ?loc (str "The type parameter " ++ Id.print id ++
str " occurs several times")
in
@@ -409,13 +409,13 @@ let register_typedef ?(local = false) isrec types =
let () = List.iter check types in
let self =
if isrec then
- let fold accu ((_, id), (params, _)) =
+ let fold accu ({v=id}, (params, _)) =
Id.Map.add id (Lib.make_kn id, List.length params) accu
in
List.fold_left fold Id.Map.empty types
else Id.Map.empty
in
- let map ((_, id), def) =
+ let map ({v=id}, def) =
let typdef = {
typdef_local = local;
typdef_expr = intern_typedef self def;
@@ -426,7 +426,7 @@ let register_typedef ?(local = false) isrec types =
let iter (id, def) = ignore (Lib.add_leaf id (inTypDef def)) in
List.iter iter types
-let register_primitive ?(local = false) (loc, id) t ml =
+let register_primitive ?(local = false) {loc;v=id} t ml =
let t = intern_open_type t in
let rec count_arrow = function
| GTypArrow (_, t) -> 1 + count_arrow t
@@ -453,7 +453,7 @@ let register_primitive ?(local = false) (loc, id) t ml =
} in
ignore (Lib.add_leaf id (inTacDef def))
-let register_open ?(local = false) (loc, qid) (params, def) =
+let register_open ?(local = false) {loc;v=qid} (params, def) =
let kn =
try Tac2env.locate_type qid
with Not_found ->
@@ -496,14 +496,13 @@ let register_open ?(local = false) (loc, qid) (params, def) =
let register_type ?local isrec types = match types with
| [qid, true, def] ->
- let (loc, _) = qid in
+ let {loc} = qid in
let () = if isrec then user_err ?loc (str "Extensions cannot be recursive") in
register_open ?local qid def
| _ ->
let map (qid, redef, def) =
- let (loc, _) = qid in
let () = if redef then
- user_err ?loc (str "Types can only be extended one by one")
+ user_err ?loc:qid.loc (str "Types can only be extended one by one")
in
(qualid_to_ident qid, def)
in
@@ -530,26 +529,26 @@ module ParseToken =
struct
let loc_of_token = function
-| SexprStr (loc, _) -> loc
-| SexprInt (loc, _) -> loc
+| SexprStr {loc} -> loc
+| SexprInt {loc} -> loc
| SexprRec (loc, _, _) -> Some loc
let parse_scope = function
-| SexprRec (_, (loc, Some id), toks) ->
+| SexprRec (_, {loc;v=Some id}, toks) ->
if Id.Map.mem id !scope_table then
Id.Map.find id !scope_table toks
else
CErrors.user_err ?loc (str "Unknown scope" ++ spc () ++ Names.Id.print id)
-| SexprStr (_, str) ->
- let v_unit = Loc.tag @@ CTacCst (AbsKn (Tuple 0)) in
+| SexprStr {v=str} ->
+ let v_unit = CAst.make @@ CTacCst (AbsKn (Tuple 0)) in
ScopeRule (Extend.Atoken (Tok.IDENT str), (fun _ -> v_unit))
| tok ->
let loc = loc_of_token tok in
CErrors.user_err ?loc (str "Invalid parsing token")
let parse_token = function
-| SexprStr (_, s) -> TacTerm s
-| SexprRec (_, (_, na), [tok]) ->
+| SexprStr {v=s} -> TacTerm s
+| SexprRec (_, {v=na}, [tok]) ->
let na = match na with None -> Anonymous | Some id -> Name id in
let scope = parse_scope tok in
TacNonTerm (na, scope)
@@ -591,11 +590,10 @@ let perform_notation syn st =
let KRule (rule, act) = get_rule tok in
let mk loc args =
let map (na, e) =
- let loc = loc_of_tacexpr e in
- ((Loc.tag ?loc @@ CPatVar na), e)
+ ((CAst.make ?loc:e.loc @@ CPatVar na), e)
in
let bnd = List.map map args in
- Loc.tag ~loc @@ CTacLet (false, bnd, syn.synext_exp)
+ CAst.make ~loc @@ CTacLet (false, bnd, syn.synext_exp)
in
let rule = Extend.Rule (rule, act mk) in
let lev = match syn.synext_lev with
@@ -659,9 +657,9 @@ let inTac2Abbreviation : abbreviation -> obj =
classify_function = classify_abbreviation}
let register_notation ?(local = false) tkn lev body = match tkn, lev with
-| [SexprRec (_, (loc, Some id), [])], None ->
+| [SexprRec (_, {loc;v=Some id}, [])], None ->
(** Tactic abbreviation *)
- let () = check_lowercase (loc, id) in
+ let () = check_lowercase CAst.(make ?loc id) in
let body = Tac2intern.globalize Id.Set.empty body in
let abbr = { abbr_body = body } in
ignore (Lib.add_leaf id (inTac2Abbreviation abbr))
@@ -780,7 +778,7 @@ let register_struct ?local str = match str with
| StrTyp (isrec, t) -> register_type ?local isrec t
| StrPrm (id, t, ml) -> register_primitive ?local id t ml
| StrSyn (tok, lev, e) -> register_notation ?local tok lev e
-| StrMut (qid, e) -> register_redefinition ?local qid e
+| StrMut (qid, e) -> register_redefinition ?local CAst.(qid.loc, qid.v) e
| StrRun e -> perform_eval e
(** Toplevel exception *)
@@ -876,7 +874,7 @@ let solve default tac =
if not status then Feedback.feedback Feedback.AddedAxiom
let call ~default e =
- let loc = loc_of_tacexpr e in
+ let loc = e.loc in
let (e, t) = intern ~strict:false e in
let () = check_unit ?loc t in
let tac = Tac2interp.interp Tac2interp.empty_environment e in
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index a92e149a85..cfb58ea383 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Loc
open Names
open Libnames
open Tac2expr
@@ -14,13 +13,13 @@ open Tac2expr
(** {5 Toplevel definitions} *)
val register_ltac : ?local:bool -> ?mut:bool -> rec_flag ->
- (Name.t located * raw_tacexpr) list -> unit
+ (Misctypes.lname * raw_tacexpr) list -> unit
val register_type : ?local:bool -> rec_flag ->
- (qualid located * redef_flag * raw_quant_typedef) list -> unit
+ (qualid CAst.t * redef_flag * raw_quant_typedef) list -> unit
val register_primitive : ?local:bool ->
- Id.t located -> raw_typexpr -> ml_tactic_name -> unit
+ Misctypes.lident -> raw_typexpr -> ml_tactic_name -> unit
val register_struct : ?local:bool -> strexpr -> unit
@@ -63,11 +62,11 @@ val tac2expr : raw_tacexpr Pcoq.Gram.entry
open Tac2qexpr
-val q_ident : Id.t located or_anti Pcoq.Gram.entry
+val q_ident : Id.t CAst.t or_anti Pcoq.Gram.entry
val q_bindings : bindings Pcoq.Gram.entry
val q_with_bindings : bindings Pcoq.Gram.entry
val q_intropattern : intro_pattern Pcoq.Gram.entry
-val q_intropatterns : intro_pattern list located Pcoq.Gram.entry
+val q_intropatterns : intro_pattern list CAst.t Pcoq.Gram.entry
val q_destruction_arg : destruction_arg Pcoq.Gram.entry
val q_induction_clause : induction_clause Pcoq.Gram.entry
val q_conversion : conversion Pcoq.Gram.entry
diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index 60f10d360f..ddffd13a31 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -27,7 +27,7 @@ type tacref =
| TacAlias of ltac_alias
type 'a or_relid =
-| RelId of qualid located
+| RelId of qualid CAst.t
| AbsKn of 'a
(** {5 Misc} *)
@@ -48,7 +48,7 @@ type raw_typexpr_r =
| CTypArrow of raw_typexpr * raw_typexpr
| CTypRef of type_constant or_tuple or_relid * raw_typexpr list
-and raw_typexpr = raw_typexpr_r located
+and raw_typexpr = raw_typexpr_r CAst.t
type raw_typedef =
| CTydDef of raw_typexpr option
@@ -78,7 +78,7 @@ type glb_typedef =
type type_scheme = int * int glb_typexpr
-type raw_quant_typedef = Id.t located list * raw_typedef
+type raw_quant_typedef = Misctypes.lident list * raw_typedef
type glb_quant_typedef = int * glb_typedef
(** {5 Term syntax} *)
@@ -93,7 +93,7 @@ type raw_patexpr_r =
| CPatRef of ltac_constructor or_tuple or_relid * raw_patexpr list
| CPatCnv of raw_patexpr * raw_typexpr
-and raw_patexpr = raw_patexpr_r located
+and raw_patexpr = raw_patexpr_r CAst.t
type raw_tacexpr_r =
| CTacAtm of atom
@@ -110,7 +110,7 @@ type raw_tacexpr_r =
| CTacSet of raw_tacexpr * ltac_projection or_relid * raw_tacexpr
| CTacExt : ('a, _) Tac2dyn.Arg.tag * 'a -> raw_tacexpr_r
-and raw_tacexpr = raw_tacexpr_r located
+and raw_tacexpr = raw_tacexpr_r CAst.t
and raw_taccase = raw_patexpr * raw_tacexpr
@@ -152,22 +152,22 @@ type exp_level =
| E0
type sexpr =
-| SexprStr of string located
-| SexprInt of int located
-| SexprRec of Loc.t * Id.t option located * sexpr list
+| SexprStr of string CAst.t
+| SexprInt of int CAst.t
+| SexprRec of Loc.t * Id.t option CAst.t * sexpr list
(** {5 Toplevel statements} *)
type strexpr =
-| StrVal of mutable_flag * rec_flag * (Name.t located * raw_tacexpr) list
+| StrVal of mutable_flag * rec_flag * (Misctypes.lname * raw_tacexpr) list
(** Term definition *)
-| StrTyp of rec_flag * (qualid located * redef_flag * raw_quant_typedef) list
+| StrTyp of rec_flag * (qualid CAst.t * redef_flag * raw_quant_typedef) list
(** Type definition *)
-| StrPrm of Id.t located * raw_typexpr * ml_tactic_name
+| StrPrm of Misctypes.lident * raw_typexpr * ml_tactic_name
(** External definition *)
| StrSyn of sexpr list * int option * raw_tacexpr
(** Syntactic extensions *)
-| StrMut of qualid located * raw_tacexpr
+| StrMut of qualid CAst.t * raw_tacexpr
(** Redefinition of mutable globals *)
| StrRun of raw_tacexpr
(** Toplevel evaluation of an expression *)
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index dc142043e8..b1dd8f7f51 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -8,6 +8,7 @@
open Pp
open Util
+open CAst
open CErrors
open Names
open Libnames
@@ -172,7 +173,7 @@ let drop_ltac2_env store =
let fresh_id env = UF.fresh env.env_cst
-let get_alias (loc, id) env =
+let get_alias {loc;v=id} env =
try Id.Map.find id env.env_als.contents
with Not_found ->
if env.env_opn then
@@ -185,10 +186,6 @@ let push_name id t env = match id with
| Anonymous -> env
| Name id -> { env with env_var = Id.Map.add id t env.env_var }
-let loc_of_tacexpr (loc, _) : Loc.t option = loc
-
-let loc_of_patexpr (loc, _) : Loc.t option = loc
-
let error_nargs_mismatch ?loc kn nargs nfound =
let cstr = Tac2env.shortest_qualid_of_constructor kn in
user_err ?loc (str "Constructor " ++ pr_qualid cstr ++ str " expects " ++
@@ -206,12 +203,12 @@ let rec subst_type subst (t : 'a glb_typexpr) = match t with
| GTypRef (qid, args) ->
GTypRef (qid, List.map (fun t -> subst_type subst t) args)
-let rec intern_type env ((loc, t) : raw_typexpr) : UF.elt glb_typexpr = match t with
-| CTypVar (Name id) -> GTypVar (get_alias (Loc.tag ?loc id) env)
+let rec intern_type env ({loc;v=t} : raw_typexpr) : UF.elt glb_typexpr = match t with
+| CTypVar (Name id) -> GTypVar (get_alias (CAst.make ?loc id) env)
| CTypVar Anonymous -> GTypVar (fresh_id env)
| CTypRef (rel, args) ->
let (kn, nparams) = match rel with
- | RelId (loc, qid) ->
+ | RelId {loc;v=qid} ->
let (dp, id) = repr_qualid qid in
if DirPath.is_empty dp && Id.Map.mem id env.env_rec then
let (kn, n) = Id.Map.find id env.env_rec in
@@ -233,9 +230,9 @@ let rec intern_type env ((loc, t) : raw_typexpr) : UF.elt glb_typexpr = match t
let nargs = List.length args in
let () =
if not (Int.equal nparams nargs) then
- let loc, qid = match rel with
+ let {loc;v=qid} = match rel with
| RelId lid -> lid
- | AbsKn (Other kn) -> loc, shortest_qualid_of_type kn
+ | AbsKn (Other kn) -> CAst.make ?loc @@ shortest_qualid_of_type kn
| AbsKn (Tuple _) -> assert false
in
user_err ?loc (strbrk "The type constructor " ++ pr_qualid qid ++
@@ -500,10 +497,10 @@ let check_unit ?loc t =
let check_redundant_clause = function
| [] -> ()
-| (p, _) :: _ -> warn_redundant_clause ?loc:(loc_of_patexpr p) ()
+| (p, _) :: _ -> warn_redundant_clause ?loc:p.loc ()
let get_variable0 mem var = match var with
-| RelId (loc, qid) ->
+| RelId {loc;v=qid} ->
let (dp, id) = repr_qualid qid in
if DirPath.is_empty dp && mem id then ArgVar CAst.(make ?loc id)
else
@@ -520,7 +517,7 @@ let get_variable env var =
get_variable0 mem var
let get_constructor env var = match var with
-| RelId (loc, qid) ->
+| RelId {loc;v=qid} ->
let c = try Some (Tac2env.locate_constructor qid) with Not_found -> None in
begin match c with
| Some knc -> Other knc
@@ -530,7 +527,7 @@ let get_constructor env var = match var with
| AbsKn knc -> knc
let get_projection var = match var with
-| RelId (loc, qid) ->
+| RelId {loc;v=qid} ->
let kn = try Tac2env.locate_projection qid with Not_found ->
user_err ?loc (pr_qualid qid ++ str " is not a projection")
in
@@ -556,7 +553,7 @@ type glb_patexpr =
| GPatVar of Name.t
| GPatRef of ltac_constructor or_tuple * glb_patexpr list
-let rec intern_patexpr env (loc, pat) = match pat with
+let rec intern_patexpr env {loc;v=pat} = match pat with
| CPatVar na -> GPatVar na
| CPatRef (qid, pl) ->
let kn = get_constructor env qid in
@@ -601,7 +598,7 @@ let add_name accu = function
| Name id -> Id.Set.add id accu
| Anonymous -> accu
-let rec ids_of_pattern accu (_, pat) = match pat with
+let rec ids_of_pattern accu {v=pat} = match pat with
| CPatVar Anonymous -> accu
| CPatVar (Name id) -> Id.Set.add id accu
| CPatRef (_, pl) ->
@@ -609,24 +606,23 @@ let rec ids_of_pattern accu (_, pat) = match pat with
| CPatCnv (pat, _) -> ids_of_pattern accu pat
let loc_of_relid = function
-| RelId (loc, _) -> loc
+| RelId {loc} -> loc
| AbsKn _ -> None
-let extract_pattern_type (loc, p as pat) = match p with
+let extract_pattern_type ({loc;v=p} as pat) = match p with
| CPatCnv (pat, ty) -> pat, Some ty
| CPatVar _ | CPatRef _ -> pat, None
(** Expand pattern: [p => t] becomes [x => match x with p => t end] *)
let expand_pattern avoid bnd =
let fold (avoid, bnd) (pat, t) =
- let na, expand = match snd pat with
+ let na, expand = match pat.v with
| CPatVar na ->
(** Don't expand variable patterns *)
na, None
| _ ->
- let loc = loc_of_patexpr pat in
let id = fresh_var avoid in
- let qid = RelId (Loc.tag ?loc (qualid_of_ident id)) in
+ let qid = RelId (CAst.make ?loc:pat.loc (qualid_of_ident id)) in
Name id, Some qid
in
let avoid = ids_of_pattern avoid pat in
@@ -638,7 +634,7 @@ let expand_pattern avoid bnd =
| None -> e
| Some qid ->
let loc = loc_of_relid qid in
- Loc.tag ?loc @@ CTacCse (Loc.tag ?loc @@ CTacRef qid, [pat, e])
+ CAst.make ?loc @@ CTacCse (CAst.make ?loc @@ CTacRef qid, [pat, e])
in
let expand e = List.fold_left fold e bnd in
let nas = List.rev_map (fun (na, _, _) -> na) bnd in
@@ -648,7 +644,7 @@ let is_alias env qid = match get_variable env qid with
| ArgArg (TacAlias _) -> true
| ArgVar _ | (ArgArg (TacConstant _)) -> false
-let rec intern_rec env (loc, e) = match e with
+let rec intern_rec env {loc;v=e} = match e with
| CTacAtm atm -> intern_atm env atm
| CTacRef qid ->
begin match get_variable env qid with
@@ -685,10 +681,10 @@ let rec intern_rec env (loc, e) = match e with
let (e, t) = intern_rec env (exp e) in
let t = List.fold_right (fun t accu -> GTypArrow (t, accu)) tl t in
(GTacFun (nas, e), t)
-| CTacApp ((loc, CTacCst qid), args) ->
+| CTacApp ({loc;v=CTacCst qid}, args) ->
let kn = get_constructor env qid in
intern_constructor env loc kn args
-| CTacApp ((_, CTacRef qid), args) when is_alias env qid ->
+| CTacApp ({v=CTacRef qid}, args) when is_alias env qid ->
let kn = match get_variable env qid with
| ArgArg (TacAlias kn) -> kn
| ArgVar _ | (ArgArg (TacConstant _)) -> assert false
@@ -696,18 +692,18 @@ let rec intern_rec env (loc, e) = match e with
let e = Tac2env.interp_alias kn in
let map arg =
(** Thunk alias arguments *)
- let loc = loc_of_tacexpr arg in
- let t_unit = Loc.tag ?loc @@ CTypRef (AbsKn (Tuple 0), []) in
- let var = Loc.tag ?loc @@ CPatCnv (Loc.tag ?loc @@ CPatVar Anonymous, t_unit) in
- Loc.tag ?loc @@ CTacFun ([var], arg)
+ let loc = arg.loc in
+ let t_unit = CAst.make ?loc @@ CTypRef (AbsKn (Tuple 0), []) in
+ let var = CAst.make ?loc @@ CPatCnv (CAst.make ?loc @@ CPatVar Anonymous, t_unit) in
+ CAst.make ?loc @@ CTacFun ([var], arg)
in
let args = List.map map args in
- intern_rec env (Loc.tag ?loc @@ CTacApp (e, args))
+ intern_rec env (CAst.make ?loc @@ CTacApp (e, args))
| CTacApp (f, args) ->
- let loc = loc_of_tacexpr f in
+ let loc = f.loc in
let (f, ft) = intern_rec env f in
let fold arg (args, t) =
- let loc = loc_of_tacexpr arg in
+ let loc = arg.loc in
let (arg, argt) = intern_rec env arg in
(arg :: args, (loc, argt) :: t)
in
@@ -726,8 +722,7 @@ let rec intern_rec env (loc, e) = match e with
if Id.Set.is_empty common then Id.Set.union ids accu
else
let id = Id.Set.choose common in
- let loc = loc_of_patexpr pat in
- user_err ?loc (str "Variable " ++ Id.print id ++ str " is bound several \
+ user_err ?loc:pat.loc (str "Variable " ++ Id.print id ++ str " is bound several \
times in this matching")
in
let ids = List.fold_left fold Id.Set.empty el in
@@ -739,7 +734,7 @@ let rec intern_rec env (loc, e) = match e with
let () = unify ?loc env t tc in
(e, tc)
| CTacSeq (e1, e2) ->
- let loc1 = loc_of_tacexpr e1 in
+ let loc1 = e1.loc in
let (e1, t1) = intern_rec env e1 in
let (e2, t2) = intern_rec env e2 in
let () = check_elt_unit loc1 env t1 in
@@ -750,7 +745,7 @@ let rec intern_rec env (loc, e) = match e with
intern_record env loc fs
| CTacPrj (e, proj) ->
let pinfo = get_projection proj in
- let loc = loc_of_tacexpr e in
+ let loc = e.loc in
let (e, t) = intern_rec env e in
let subst = Array.init pinfo.pdata_prms (fun _ -> fresh_id env) in
let params = Array.map_to_list (fun i -> GTypVar i) subst in
@@ -764,7 +759,7 @@ let rec intern_rec env (loc, e) = match e with
let () =
if not pinfo.pdata_mutb then
let loc = match proj with
- | RelId (loc, _) -> loc
+ | RelId {CAst.loc} -> loc
| AbsKn _ -> None
in
user_err ?loc (str "Field is not mutable")
@@ -806,10 +801,9 @@ let rec intern_rec env (loc, e) = match e with
(e, tpe)
and intern_rec_with_constraint env e exp =
- let loc = loc_of_tacexpr e in
- let (e, t) = intern_rec env e in
- let () = unify ?loc env t exp in
- e
+ let (er, t) = intern_rec env e in
+ let () = unify ?loc:e.loc env t exp in
+ er
and intern_let env loc ids el e =
let avoid = Id.Set.union ids (Id.Map.domain env.env_var) in
@@ -837,11 +831,10 @@ and intern_let env loc ids el e =
and intern_let_rec env loc ids el e =
let map env (pat, t, e) =
- let (loc, pat) = pat in
- let na = match pat with
+ let na = match pat.v with
| CPatVar na -> na
| CPatRef _ | CPatCnv _ ->
- user_err ?loc (str "This kind of pattern is forbidden in let-rec bindings")
+ user_err ?loc:pat.loc (str "This kind of pattern is forbidden in let-rec bindings")
in
let id = fresh_id env in
let env = push_name na (monomorphic (GTypVar id)) env in
@@ -849,7 +842,7 @@ and intern_let_rec env loc ids el e =
in
let (env, el) = List.fold_map map env el in
let fold (loc, na, tc, e, id) (el, tl) =
- let loc_e = loc_of_tacexpr e in
+ let loc_e = e.loc in
let (e, t) = intern_rec env e in
let () =
if not (is_rec_rhs e) then
@@ -891,7 +884,7 @@ and intern_case env loc e pl =
(GTacCse (e', Other kn, [||], [||]), GTypVar r)
| PKind_variant kn ->
let subst, tc = fresh_reftype env kn in
- let () = unify ?loc:(loc_of_tacexpr e) env t tc in
+ let () = unify ?loc:e.loc env t tc in
let (nconst, nnonconst, arities) = match kn with
| Tuple 0 -> 1, 0, [0]
| Tuple n -> 0, 1, [n]
@@ -907,9 +900,9 @@ and intern_case env loc e pl =
let rec intern_branch = function
| [] -> ()
| (pat, br) :: rem ->
- let tbr = match snd pat with
+ let tbr = match pat.v with
| CPatVar (Name _) ->
- let loc = loc_of_patexpr pat in
+ let loc = pat.loc in
todo ?loc ()
| CPatVar Anonymous ->
let () = check_redundant_clause rem in
@@ -932,7 +925,7 @@ and intern_case env loc e pl =
let _ = List.fold_left fill (0, 0) arities in
brT
| CPatRef (qid, args) ->
- let loc = loc_of_patexpr pat in
+ let loc = pat.loc in
let knc = get_constructor env qid in
let kn', index, arity = match knc with
| Tuple n -> Tuple n, 0, List.init n (fun i -> GTypVar i)
@@ -946,8 +939,8 @@ and intern_case env loc e pl =
invalid_pattern ?loc kn kn'
in
let get_id pat = match pat with
- | _, CPatVar na -> na
- | loc, _ -> todo ?loc ()
+ | {v=CPatVar na} -> na
+ | {loc} -> todo ?loc ()
in
let ids = List.map get_id args in
let nids = List.length ids in
@@ -978,7 +971,7 @@ and intern_case env loc e pl =
| CPatCnv _ ->
user_err ?loc (str "Pattern not handled yet")
in
- let () = unify ?loc:(loc_of_tacexpr br) env tbr ret in
+ let () = unify ?loc:br.loc env tbr ret in
intern_branch rem
in
let () = intern_branch pl in
@@ -995,7 +988,7 @@ and intern_case env loc e pl =
(ce, ret)
| PKind_open kn ->
let subst, tc = fresh_reftype env (Other kn) in
- let () = unify ?loc:(loc_of_tacexpr e) env t tc in
+ let () = unify ?loc:e.loc env t tc in
let ret = GTypVar (fresh_id env) in
let rec intern_branch map = function
| [] ->
@@ -1014,7 +1007,7 @@ and intern_case env loc e pl =
| GPatRef _ ->
user_err ?loc (str "TODO: Unhandled match case") (** FIXME *)
in
- let loc = loc_of_patexpr pat in
+ let loc = pat.loc in
let knc = match knc with
| Other knc -> knc
| Tuple n -> invalid_pattern ?loc (Other kn) (Tuple n)
@@ -1080,7 +1073,7 @@ and intern_constructor env loc kn args = match kn with
and intern_record env loc fs =
let map (proj, e) =
let loc = match proj with
- | RelId (loc, _) -> loc
+ | RelId {CAst.loc} -> loc
| AbsKn _ -> None
in
let proj = get_projection proj in
@@ -1213,24 +1206,24 @@ let check_subtype t1 t2 =
(** Globalization *)
let get_projection0 var = match var with
-| RelId (loc, qid) ->
+| RelId {CAst.loc;v=qid} ->
let kn = try Tac2env.locate_projection qid with Not_found ->
user_err ?loc (pr_qualid qid ++ str " is not a projection")
in
kn
| AbsKn kn -> kn
-let rec globalize ids (loc, er as e) = match er with
+let rec globalize ids ({loc;v=er} as e) = match er with
| CTacAtm _ -> e
| CTacRef ref ->
let mem id = Id.Set.mem id ids in
begin match get_variable0 mem ref with
| ArgVar _ -> e
- | ArgArg kn -> Loc.tag ?loc @@ CTacRef (AbsKn kn)
+ | ArgArg kn -> CAst.make ?loc @@ CTacRef (AbsKn kn)
end
| CTacCst qid ->
let knc = get_constructor () qid in
- Loc.tag ?loc @@ CTacCst (AbsKn knc)
+ CAst.make ?loc @@ CTacCst (AbsKn knc)
| CTacFun (bnd, e) ->
let fold (pats, accu) pat =
let accu = ids_of_pattern accu pat in
@@ -1240,11 +1233,11 @@ let rec globalize ids (loc, er as e) = match er with
let bnd, ids = List.fold_left fold ([], ids) bnd in
let bnd = List.rev bnd in
let e = globalize ids e in
- Loc.tag ?loc @@ CTacFun (bnd, e)
+ CAst.make ?loc @@ CTacFun (bnd, e)
| CTacApp (e, el) ->
let e = globalize ids e in
let el = List.map (fun e -> globalize ids e) el in
- Loc.tag ?loc @@ CTacApp (e, el)
+ CAst.make ?loc @@ CTacApp (e, el)
| CTacLet (isrec, bnd, e) ->
let fold accu (pat, _) = ids_of_pattern accu pat in
let ext = List.fold_left fold Id.Set.empty bnd in
@@ -1256,34 +1249,34 @@ let rec globalize ids (loc, er as e) = match er with
(qid, globalize ids e)
in
let bnd = List.map map bnd in
- Loc.tag ?loc @@ CTacLet (isrec, bnd, e)
+ CAst.make ?loc @@ CTacLet (isrec, bnd, e)
| CTacCnv (e, t) ->
let e = globalize ids e in
- Loc.tag ?loc @@ CTacCnv (e, t)
+ CAst.make ?loc @@ CTacCnv (e, t)
| CTacSeq (e1, e2) ->
let e1 = globalize ids e1 in
let e2 = globalize ids e2 in
- Loc.tag ?loc @@ CTacSeq (e1, e2)
+ CAst.make ?loc @@ CTacSeq (e1, e2)
| CTacCse (e, bl) ->
let e = globalize ids e in
let bl = List.map (fun b -> globalize_case ids b) bl in
- Loc.tag ?loc @@ CTacCse (e, bl)
+ CAst.make ?loc @@ CTacCse (e, bl)
| CTacRec r ->
let map (p, e) =
let p = get_projection0 p in
let e = globalize ids e in
(AbsKn p, e)
in
- Loc.tag ?loc @@ CTacRec (List.map map r)
+ CAst.make ?loc @@ CTacRec (List.map map r)
| CTacPrj (e, p) ->
let e = globalize ids e in
let p = get_projection0 p in
- Loc.tag ?loc @@ CTacPrj (e, AbsKn p)
+ CAst.make ?loc @@ CTacPrj (e, AbsKn p)
| CTacSet (e, p, e') ->
let e = globalize ids e in
let p = get_projection0 p in
let e' = globalize ids e' in
- Loc.tag ?loc @@ CTacSet (e, AbsKn p, e')
+ CAst.make ?loc @@ CTacSet (e, AbsKn p, e')
| CTacExt (tag, arg) ->
let arg = str (Tac2dyn.Arg.repr tag) in
CErrors.user_err ?loc (str "Cannot globalize generic arguments of type" ++ spc () ++ arg)
@@ -1291,16 +1284,16 @@ let rec globalize ids (loc, er as e) = match er with
and globalize_case ids (p, e) =
(globalize_pattern ids p, globalize ids e)
-and globalize_pattern ids (loc, pr as p) = match pr with
+and globalize_pattern ids ({loc;v=pr} as p) = match pr with
| CPatVar _ -> p
| CPatRef (cst, pl) ->
let knc = get_constructor () cst in
let cst = AbsKn knc in
let pl = List.map (fun p -> globalize_pattern ids p) pl in
- Loc.tag ?loc @@ CPatRef (cst, pl)
+ CAst.make ?loc @@ CPatRef (cst, pl)
| CPatCnv (pat, ty) ->
let pat = globalize_pattern ids pat in
- Loc.tag ?loc @@ CPatCnv (pat, ty)
+ CAst.make ?loc @@ CPatCnv (pat, ty)
(** Kernel substitution *)
@@ -1407,16 +1400,16 @@ let subst_or_relid subst ref = match ref with
let kn' = subst_or_tuple subst_kn subst kn in
if kn' == kn then ref else AbsKn kn'
-let rec subst_rawtype subst (loc, tr as t) = match tr with
+let rec subst_rawtype subst ({loc;v=tr} as t) = match tr with
| CTypVar _ -> t
| CTypArrow (t1, t2) ->
let t1' = subst_rawtype subst t1 in
let t2' = subst_rawtype subst t2 in
- if t1' == t1 && t2' == t2 then t else Loc.tag ?loc @@ CTypArrow (t1', t2')
+ if t1' == t1 && t2' == t2 then t else CAst.make ?loc @@ CTypArrow (t1', t2')
| CTypRef (ref, tl) ->
let ref' = subst_or_relid subst ref in
let tl' = List.smartmap (fun t -> subst_rawtype subst t) tl in
- if ref' == ref && tl' == tl then t else Loc.tag ?loc @@ CTypRef (ref', tl')
+ if ref' == ref && tl' == tl then t else CAst.make ?loc @@ CTypRef (ref', tl')
let subst_tacref subst ref = match ref with
| RelId _ -> ref
@@ -1433,35 +1426,35 @@ let subst_projection subst prj = match prj with
let kn' = subst_kn subst kn in
if kn' == kn then prj else AbsKn kn'
-let rec subst_rawpattern subst (loc, pr as p) = match pr with
+let rec subst_rawpattern subst ({loc;v=pr} as p) = match pr with
| CPatVar _ -> p
| CPatRef (c, pl) ->
let pl' = List.smartmap (fun p -> subst_rawpattern subst p) pl in
let c' = subst_or_relid subst c in
- if pl' == pl && c' == c then p else Loc.tag ?loc @@ CPatRef (c', pl')
+ if pl' == pl && c' == c then p else CAst.make ?loc @@ CPatRef (c', pl')
| CPatCnv (pat, ty) ->
let pat' = subst_rawpattern subst pat in
let ty' = subst_rawtype subst ty in
- if pat' == pat && ty' == ty then p else Loc.tag ?loc @@ CPatCnv (pat', ty')
+ if pat' == pat && ty' == ty then p else CAst.make ?loc @@ CPatCnv (pat', ty')
(** Used for notations *)
-let rec subst_rawexpr subst (loc, tr as t) = match tr with
+let rec subst_rawexpr subst ({loc;v=tr} as t) = match tr with
| CTacAtm _ -> t
| CTacRef ref ->
let ref' = subst_tacref subst ref in
- if ref' == ref then t else Loc.tag ?loc @@ CTacRef ref'
+ if ref' == ref then t else CAst.make ?loc @@ CTacRef ref'
| CTacCst ref ->
let ref' = subst_or_relid subst ref in
- if ref' == ref then t else Loc.tag ?loc @@ CTacCst ref'
+ if ref' == ref then t else CAst.make ?loc @@ CTacCst ref'
| CTacFun (bnd, e) ->
let map pat = subst_rawpattern subst pat in
let bnd' = List.smartmap map bnd in
let e' = subst_rawexpr subst e in
- if bnd' == bnd && e' == e then t else Loc.tag ?loc @@ CTacFun (bnd', e')
+ if bnd' == bnd && e' == e then t else CAst.make ?loc @@ CTacFun (bnd', e')
| CTacApp (e, el) ->
let e' = subst_rawexpr subst e in
let el' = List.smartmap (fun e -> subst_rawexpr subst e) el in
- if e' == e && el' == el then t else Loc.tag ?loc @@ CTacApp (e', el')
+ if e' == e && el' == el then t else CAst.make ?loc @@ CTacApp (e', el')
| CTacLet (isrec, bnd, e) ->
let map (na, e as p) =
let na' = subst_rawpattern subst na in
@@ -1470,15 +1463,15 @@ let rec subst_rawexpr subst (loc, tr as t) = match tr with
in
let bnd' = List.smartmap map bnd in
let e' = subst_rawexpr subst e in
- if bnd' == bnd && e' == e then t else Loc.tag ?loc @@ CTacLet (isrec, bnd', e')
+ if bnd' == bnd && e' == e then t else CAst.make ?loc @@ CTacLet (isrec, bnd', e')
| CTacCnv (e, c) ->
let e' = subst_rawexpr subst e in
let c' = subst_rawtype subst c in
- if c' == c && e' == e then t else Loc.tag ?loc @@ CTacCnv (e', c')
+ if c' == c && e' == e then t else CAst.make ?loc @@ CTacCnv (e', c')
| CTacSeq (e1, e2) ->
let e1' = subst_rawexpr subst e1 in
let e2' = subst_rawexpr subst e2 in
- if e1' == e1 && e2' == e2 then t else Loc.tag ?loc @@ CTacSeq (e1', e2')
+ if e1' == e1 && e2' == e2 then t else CAst.make ?loc @@ CTacSeq (e1', e2')
| CTacCse (e, bl) ->
let map (p, e as x) =
let p' = subst_rawpattern subst p in
@@ -1487,7 +1480,7 @@ let rec subst_rawexpr subst (loc, tr as t) = match tr with
in
let e' = subst_rawexpr subst e in
let bl' = List.smartmap map bl in
- if e' == e && bl' == bl then t else Loc.tag ?loc @@ CTacCse (e', bl')
+ if e' == e && bl' == bl then t else CAst.make ?loc @@ CTacCse (e', bl')
| CTacRec el ->
let map (prj, e as p) =
let prj' = subst_projection subst prj in
@@ -1495,16 +1488,16 @@ let rec subst_rawexpr subst (loc, tr as t) = match tr with
if prj' == prj && e' == e then p else (prj', e')
in
let el' = List.smartmap map el in
- if el' == el then t else Loc.tag ?loc @@ CTacRec el'
+ if el' == el then t else CAst.make ?loc @@ CTacRec el'
| CTacPrj (e, prj) ->
let prj' = subst_projection subst prj in
let e' = subst_rawexpr subst e in
- if prj' == prj && e' == e then t else Loc.tag ?loc @@ CTacPrj (e', prj')
+ if prj' == prj && e' == e then t else CAst.make ?loc @@ CTacPrj (e', prj')
| CTacSet (e, prj, r) ->
let prj' = subst_projection subst prj in
let e' = subst_rawexpr subst e in
let r' = subst_rawexpr subst r in
- if prj' == prj && e' == e && r' == r then t else Loc.tag ?loc @@ CTacSet (e', prj', r')
+ if prj' == prj && e' == e && r' == r then t else CAst.make ?loc @@ CTacSet (e', prj', r')
| CTacExt _ -> assert false (** Should not be generated by globalization *)
(** Registering *)
@@ -1520,7 +1513,7 @@ let () =
else { env with env_str = false }
| Some env -> env
in
- let loc = loc_of_tacexpr tac in
+ let loc = tac.loc in
let (tac, t) = intern_rec env tac in
let () = check_elt_unit loc env t in
(ist, tac)
diff --git a/src/tac2intern.mli b/src/tac2intern.mli
index 4b02f91caa..d646b5cda5 100644
--- a/src/tac2intern.mli
+++ b/src/tac2intern.mli
@@ -10,9 +10,6 @@ open Names
open Mod_subst
open Tac2expr
-val loc_of_tacexpr : raw_tacexpr -> Loc.t option
-val loc_of_patexpr : raw_patexpr -> Loc.t option
-
val intern : strict:bool -> raw_tacexpr -> glb_tacexpr * type_scheme
val intern_typedef : (KerName.t * int) Id.Map.t -> raw_quant_typedef -> glb_quant_typedef
val intern_open_type : raw_typexpr -> type_scheme
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index 2f6c97f08b..05b9f4141f 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Loc
open Names
open Tac2expr
@@ -15,65 +14,65 @@ open Tac2expr
type 'a or_anti =
| QExpr of 'a
-| QAnti of Id.t located
+| QAnti of Id.t CAst.t
type quantified_hypothesis =
-| QAnonHyp of int located
-| QNamedHyp of Id.t located
+| QAnonHyp of int CAst.t
+| QNamedHyp of Id.t CAst.t
type bindings_r =
| QImplicitBindings of Constrexpr.constr_expr list
-| QExplicitBindings of (quantified_hypothesis located or_anti * Constrexpr.constr_expr) located list
+| QExplicitBindings of (quantified_hypothesis CAst.t or_anti * Constrexpr.constr_expr) CAst.t list
| QNoBindings
-type bindings = bindings_r located
+type bindings = bindings_r CAst.t
type intro_pattern_r =
| QIntroForthcoming of bool
| QIntroNaming of intro_pattern_naming
| QIntroAction of intro_pattern_action
and intro_pattern_naming_r =
-| QIntroIdentifier of Id.t located or_anti
-| QIntroFresh of Id.t located or_anti
+| QIntroIdentifier of Id.t CAst.t or_anti
+| QIntroFresh of Id.t CAst.t or_anti
| QIntroAnonymous
and intro_pattern_action_r =
| QIntroWildcard
| QIntroOrAndPattern of or_and_intro_pattern
-| QIntroInjection of intro_pattern list located
+| QIntroInjection of intro_pattern list CAst.t
(* | QIntroApplyOn of Empty.t (** Not implemented yet *) *)
| QIntroRewrite of bool
and or_and_intro_pattern_r =
-| QIntroOrPattern of intro_pattern list located list
-| QIntroAndPattern of intro_pattern list located
+| QIntroOrPattern of intro_pattern list CAst.t list
+| QIntroAndPattern of intro_pattern list CAst.t
-and intro_pattern = intro_pattern_r located
-and intro_pattern_naming = intro_pattern_naming_r located
-and intro_pattern_action = intro_pattern_action_r located
-and or_and_intro_pattern = or_and_intro_pattern_r located
+and intro_pattern = intro_pattern_r CAst.t
+and intro_pattern_naming = intro_pattern_naming_r CAst.t
+and intro_pattern_action = intro_pattern_action_r CAst.t
+and or_and_intro_pattern = or_and_intro_pattern_r CAst.t
type occurrences_r =
| QAllOccurrences
-| QAllOccurrencesBut of int located or_anti list
+| QAllOccurrencesBut of int CAst.t or_anti list
| QNoOccurrences
-| QOnlyOccurrences of int located or_anti list
+| QOnlyOccurrences of int CAst.t or_anti list
-type occurrences = occurrences_r located
+type occurrences = occurrences_r CAst.t
-type hyp_location = (occurrences * Id.t located or_anti) * Locus.hyp_location_flag
+type hyp_location = (occurrences * Id.t CAst.t or_anti) * Locus.hyp_location_flag
type clause_r =
{ q_onhyps : hyp_location list option; q_concl_occs : occurrences; }
-type clause = clause_r located
+type clause = clause_r CAst.t
-type constr_with_bindings = (Constrexpr.constr_expr * bindings) located
+type constr_with_bindings = (Constrexpr.constr_expr * bindings) CAst.t
type destruction_arg_r =
| QElimOnConstr of constr_with_bindings
-| QElimOnIdent of Id.t located
-| QElimOnAnonHyp of int located
+| QElimOnIdent of Id.t CAst.t
+| QElimOnAnonHyp of int CAst.t
-type destruction_arg = destruction_arg_r located
+type destruction_arg = destruction_arg_r CAst.t
type induction_clause_r = {
indcl_arg : destruction_arg;
@@ -82,33 +81,33 @@ type induction_clause_r = {
indcl_in : clause option;
}
-type induction_clause = induction_clause_r located
+type induction_clause = induction_clause_r CAst.t
type conversion_r =
| QConvert of Constrexpr.constr_expr
| QConvertWith of Constrexpr.constr_expr * Constrexpr.constr_expr
-type conversion = conversion_r located
+type conversion = conversion_r CAst.t
type multi_r =
-| QPrecisely of int located
-| QUpTo of int located
+| QPrecisely of int CAst.t
+| QUpTo of int CAst.t
| QRepeatStar
| QRepeatPlus
-type multi = multi_r located
+type multi = multi_r CAst.t
type rewriting_r = {
- rew_orient : bool option located;
+ rew_orient : bool option CAst.t;
rew_repeat : multi;
rew_equatn : constr_with_bindings;
}
-type rewriting = rewriting_r located
+type rewriting = rewriting_r CAst.t
type dispatch_r = raw_tacexpr option list * (raw_tacexpr option * raw_tacexpr option list) option
-type dispatch = dispatch_r located
+type dispatch = dispatch_r CAst.t
type red_flag_r =
| QBeta
@@ -117,52 +116,52 @@ type red_flag_r =
| QFix
| QCofix
| QZeta
-| QConst of Libnames.reference or_anti list located
-| QDeltaBut of Libnames.reference or_anti list located
+| QConst of Libnames.reference or_anti list CAst.t
+| QDeltaBut of Libnames.reference or_anti list CAst.t
-type red_flag = red_flag_r located
+type red_flag = red_flag_r CAst.t
-type strategy_flag = red_flag list located
+type strategy_flag = red_flag list CAst.t
type constr_match_pattern_r =
| QConstrMatchPattern of Constrexpr.constr_expr
| QConstrMatchContext of Id.t option * Constrexpr.constr_expr
-type constr_match_pattern = constr_match_pattern_r located
+type constr_match_pattern = constr_match_pattern_r CAst.t
-type constr_match_branch = (constr_match_pattern * raw_tacexpr) located
+type constr_match_branch = (constr_match_pattern * raw_tacexpr) CAst.t
-type constr_matching = constr_match_branch list located
+type constr_matching = constr_match_branch list CAst.t
type goal_match_pattern_r = {
q_goal_match_concl : constr_match_pattern;
q_goal_match_hyps : (Misctypes.lname * constr_match_pattern) list;
}
-type goal_match_pattern = goal_match_pattern_r located
+type goal_match_pattern = goal_match_pattern_r CAst.t
-type goal_match_branch = (goal_match_pattern * raw_tacexpr) located
+type goal_match_branch = (goal_match_pattern * raw_tacexpr) CAst.t
-type goal_matching = goal_match_branch list located
+type goal_matching = goal_match_branch list CAst.t
type hintdb_r =
| QHintAll
-| QHintDbs of Id.t located or_anti list
+| QHintDbs of Id.t CAst.t or_anti list
-type hintdb = hintdb_r located
+type hintdb = hintdb_r CAst.t
type move_location_r =
-| QMoveAfter of Id.t located or_anti
-| QMoveBefore of Id.t located or_anti
+| QMoveAfter of Id.t CAst.t or_anti
+| QMoveBefore of Id.t CAst.t or_anti
| QMoveFirst
| QMoveLast
-type move_location = move_location_r located
+type move_location = move_location_r CAst.t
-type pose = (Id.t located or_anti option * Constrexpr.constr_expr) located
+type pose = (Id.t CAst.t or_anti option * Constrexpr.constr_expr) CAst.t
type assertion_r =
| QAssertType of intro_pattern option * Constrexpr.constr_expr * raw_tacexpr option
-| QAssertValue of Id.t located or_anti * Constrexpr.constr_expr
+| QAssertValue of Id.t CAst.t or_anti * Constrexpr.constr_expr
-type assertion = assertion_r located
+type assertion = assertion_r CAst.t
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index 829f13344c..e986bfc393 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -9,6 +9,7 @@
open Pp
open Names
open Util
+open CAst
open Tac2dyn
open Tac2expr
open Tac2qexpr
@@ -38,12 +39,12 @@ let control_core n = kername control_prefix n
let pattern_core n = kername pattern_prefix n
let global_ref ?loc kn =
- Loc.tag ?loc @@ CTacRef (AbsKn (TacConstant kn))
+ CAst.make ?loc @@ CTacRef (AbsKn (TacConstant kn))
let constructor ?loc kn args =
- let cst = Loc.tag ?loc @@ CTacCst (AbsKn (Other kn)) in
+ let cst = CAst.make ?loc @@ CTacCst (AbsKn (Other kn)) in
if List.is_empty args then cst
- else Loc.tag ?loc @@ CTacApp (cst, args)
+ else CAst.make ?loc @@ CTacApp (cst, args)
let std_constructor ?loc name args =
constructor ?loc (std_core name) args
@@ -53,44 +54,44 @@ let std_proj ?loc name =
let thunk e =
let t_unit = coq_core "unit" in
- let loc = Tac2intern.loc_of_tacexpr e in
- let ty = Loc.tag ?loc @@ CTypRef (AbsKn (Other t_unit), []) in
- let pat = Loc.tag ?loc @@ CPatVar (Anonymous) in
- let pat = Loc.tag ?loc @@ CPatCnv (pat, ty) in
- Loc.tag ?loc @@ CTacFun ([pat], e)
+ let loc = e.loc in
+ let ty = CAst.make?loc @@ CTypRef (AbsKn (Other t_unit), []) in
+ let pat = CAst.make ?loc @@ CPatVar (Anonymous) in
+ let pat = CAst.make ?loc @@ CPatCnv (pat, ty) in
+ CAst.make ?loc @@ CTacFun ([pat], e)
-let of_pair f g (loc, (e1, e2)) =
- Loc.tag ?loc @@ CTacApp (Loc.tag ?loc @@ CTacCst (AbsKn (Tuple 2)), [f e1; g e2])
+let of_pair f g {loc;v=(e1, e2)} =
+ CAst.make ?loc @@ CTacApp (CAst.make ?loc @@ CTacCst (AbsKn (Tuple 2)), [f e1; g e2])
let of_tuple ?loc el = match el with
| [] ->
- Loc.tag ?loc @@ CTacCst (AbsKn (Tuple 0))
+ CAst.make ?loc @@ CTacCst (AbsKn (Tuple 0))
| [e] -> e
| el ->
let len = List.length el in
- Loc.tag ?loc @@ CTacApp (Loc.tag ?loc @@ CTacCst (AbsKn (Tuple len)), el)
+ CAst.make ?loc @@ CTacApp (CAst.make ?loc @@ CTacCst (AbsKn (Tuple len)), el)
-let of_int (loc, n) =
- Loc.tag ?loc @@ CTacAtm (AtmInt n)
+let of_int {loc;v=n} =
+ CAst.make ?loc @@ CTacAtm (AtmInt n)
let of_option ?loc f opt = match opt with
| None -> constructor ?loc (coq_core "None") []
| Some e -> constructor ?loc (coq_core "Some") [f e]
let inj_wit ?loc wit x =
- Loc.tag ?loc @@ CTacExt (wit, x)
+ CAst.make ?loc @@ CTacExt (wit, x)
-let of_variable (loc, id) =
+let of_variable {loc;v=id} =
let qid = Libnames.qualid_of_ident id in
if Tac2env.is_constructor qid then
CErrors.user_err ?loc (str "Invalid identifier")
- else Loc.tag ?loc @@ CTacRef (RelId (Loc.tag ?loc qid))
+ else CAst.make ?loc @@ CTacRef (RelId (CAst.make ?loc qid))
let of_anti f = function
| QExpr x -> f x
| QAnti id -> of_variable id
-let of_ident (loc, id) = inj_wit ?loc wit_ident id
+let of_ident {loc;v=id} = inj_wit ?loc wit_ident id
let of_constr c =
let loc = Constrexpr_ops.constr_loc c in
@@ -109,11 +110,11 @@ let rec of_list ?loc f = function
| e :: l ->
constructor ?loc (coq_core "::") [f e; of_list ?loc f l]
-let of_qhyp (loc, h) = match h with
+let of_qhyp {loc;v=h} = match h with
| QAnonHyp n -> std_constructor ?loc "AnonHyp" [of_int n]
| QNamedHyp id -> std_constructor ?loc "NamedHyp" [of_ident id]
-let of_bindings (loc, b) = match b with
+let of_bindings {loc;v=b} = match b with
| QNoBindings ->
std_constructor ?loc "NoBindings" []
| QImplicitBindings tl ->
@@ -124,7 +125,7 @@ let of_bindings (loc, b) = match b with
let of_constr_with_bindings c = of_pair of_open_constr of_bindings c
-let rec of_intro_pattern (loc, pat) = match pat with
+let rec of_intro_pattern {loc;v=pat} = match pat with
| QIntroForthcoming b ->
std_constructor ?loc "IntroForthcoming" [of_bool b]
| QIntroNaming iname ->
@@ -132,7 +133,7 @@ let rec of_intro_pattern (loc, pat) = match pat with
| QIntroAction iact ->
std_constructor ?loc "IntroAction" [of_intro_pattern_action iact]
-and of_intro_pattern_naming (loc, pat) = match pat with
+and of_intro_pattern_naming {loc;v=pat} = match pat with
| QIntroIdentifier id ->
std_constructor ?loc "IntroIdentifier" [of_anti of_ident id]
| QIntroFresh id ->
@@ -140,7 +141,7 @@ and of_intro_pattern_naming (loc, pat) = match pat with
| QIntroAnonymous ->
std_constructor ?loc "IntroAnonymous" []
-and of_intro_pattern_action (loc, pat) = match pat with
+and of_intro_pattern_action {loc;v=pat} = match pat with
| QIntroWildcard ->
std_constructor ?loc "IntroWildcard" []
| QIntroOrAndPattern pat ->
@@ -150,13 +151,13 @@ and of_intro_pattern_action (loc, pat) = match pat with
| QIntroRewrite b ->
std_constructor ?loc "IntroRewrite" [of_bool ?loc b]
-and of_or_and_intro_pattern (loc, pat) = match pat with
+and of_or_and_intro_pattern {loc;v=pat} = match pat with
| QIntroOrPattern ill ->
std_constructor ?loc "IntroOrPattern" [of_list ?loc of_intro_patterns ill]
| QIntroAndPattern il ->
std_constructor ?loc "IntroAndPattern" [of_intro_patterns il]
-and of_intro_patterns (loc, l) =
+and of_intro_patterns {loc;v=l} =
of_list ?loc of_intro_pattern l
let of_hyp_location_flag ?loc = function
@@ -164,7 +165,7 @@ let of_hyp_location_flag ?loc = function
| Locus.InHypTypeOnly -> std_constructor ?loc "InHypTypeOnly" []
| Locus.InHypValueOnly -> std_constructor ?loc "InHypValueOnly" []
-let of_occurrences (loc, occ) = match occ with
+let of_occurrences {loc;v=occ} = match occ with
| QAllOccurrences -> std_constructor ?loc "AllOccurrences" []
| QAllOccurrencesBut occs ->
let map occ = of_anti of_int occ in
@@ -183,27 +184,27 @@ let of_hyp_location ?loc ((occs, id), flag) =
of_hyp_location_flag ?loc flag;
]
-let of_clause (loc, cl) =
+let of_clause {loc;v=cl} =
let hyps = of_option ?loc (fun l -> of_list ?loc of_hyp_location l) cl.q_onhyps in
let concl = of_occurrences cl.q_concl_occs in
- Loc.tag ?loc @@ CTacRec ([
+ CAst.make ?loc @@ CTacRec ([
std_proj "on_hyps", hyps;
std_proj "on_concl", concl;
])
-let of_destruction_arg (loc, arg) = match arg with
+let of_destruction_arg {loc;v=arg} = match arg with
| QElimOnConstr c ->
let arg = thunk (of_constr_with_bindings c) in
std_constructor ?loc "ElimOnConstr" [arg]
| QElimOnIdent id -> std_constructor ?loc "ElimOnIdent" [of_ident id]
| QElimOnAnonHyp n -> std_constructor ?loc "ElimOnAnonHyp" [of_int n]
-let of_induction_clause (loc, cl) =
+let of_induction_clause {loc;v=cl} =
let arg = of_destruction_arg cl.indcl_arg in
let eqn = of_option ?loc of_intro_pattern_naming cl.indcl_eqn in
let as_ = of_option ?loc of_or_and_intro_pattern cl.indcl_as in
let in_ = of_option ?loc of_clause cl.indcl_in in
- Loc.tag ?loc @@ CTacRec ([
+ CAst.make ?loc @@ CTacRec ([
std_proj "indcl_arg", arg;
std_proj "indcl_eqn", eqn;
std_proj "indcl_as", as_;
@@ -238,24 +239,24 @@ let abstract_vars loc vars tac =
| Anonymous -> (n + 1, accu)
| Name _ ->
let get = global_ref ?loc (kername array_prefix "get") in
- let args = [of_variable (loc, id0); of_int (loc, n)] in
- let e = Loc.tag ?loc @@ CTacApp (get, args) in
- let accu = (Loc.tag ?loc @@ CPatVar na, e) :: accu in
+ let args = [of_variable CAst.(make ?loc id0); of_int CAst.(make ?loc n)] in
+ let e = CAst.make ?loc @@ CTacApp (get, args) in
+ let accu = (CAst.make ?loc @@ CPatVar na, e) :: accu in
(n + 1, accu)
in
let (_, bnd) = List.fold_left build_bindings (0, []) vars in
- let tac = Loc.tag ?loc @@ CTacLet (false, bnd, tac) in
+ let tac = CAst.make ?loc @@ CTacLet (false, bnd, tac) in
(Name id0, tac)
in
- Loc.tag ?loc @@ CTacFun ([Loc.tag ?loc @@ CPatVar na], tac)
+ CAst.make ?loc @@ CTacFun ([CAst.make ?loc @@ CPatVar na], tac)
let of_pattern p =
inj_wit ?loc:p.CAst.loc wit_pattern p
-let of_conversion (loc, c) = match c with
+let of_conversion {loc;v=c} = match c with
| QConvert c ->
let pat = of_option ?loc of_pattern None in
- let c = Loc.tag ?loc @@ CTacFun ([Loc.tag ?loc @@ CPatVar Anonymous], of_constr c) in
+ let c = CAst.make ?loc @@ CTacFun ([CAst.make ?loc @@ CPatVar Anonymous], of_constr c) in
of_tuple ?loc [pat; c]
| QConvertWith (pat, c) ->
let vars = pattern_vars pat in
@@ -266,7 +267,7 @@ let of_conversion (loc, c) = match c with
let c = abstract_vars loc vars c in
of_tuple [pat; c]
-let of_repeat (loc, r) = match r with
+let of_repeat {loc;v=r} = match r with
| QPrecisely n -> std_constructor ?loc "Precisely" [of_int n]
| QUpTo n -> std_constructor ?loc "UpTo" [of_int n]
| QRepeatStar -> std_constructor ?loc "RepeatStar" []
@@ -276,14 +277,14 @@ let of_orient loc b =
if b then std_constructor ?loc "LTR" []
else std_constructor ?loc "RTL" []
-let of_rewriting (loc, rew) =
+let of_rewriting {loc;v=rew} =
let orient =
- let (loc, orient) = rew.rew_orient in
+ let {loc;v=orient} = rew.rew_orient in
of_option ?loc (fun b -> of_orient loc b) orient
in
let repeat = of_repeat rew.rew_repeat in
let equatn = thunk (of_constr_with_bindings rew.rew_equatn) in
- Loc.tag ?loc @@ CTacRec ([
+ CAst.make ?loc @@ CTacRec ([
std_proj "rew_orient", orient;
std_proj "rew_repeat", repeat;
std_proj "rew_equatn", equatn;
@@ -291,42 +292,42 @@ let of_rewriting (loc, rew) =
let of_hyp ?loc id =
let hyp = global_ref ?loc (control_core "hyp") in
- Loc.tag ?loc @@ CTacApp (hyp, [of_ident id])
+ CAst.make ?loc @@ CTacApp (hyp, [of_ident id])
let of_exact_hyp ?loc id =
let refine = global_ref ?loc (control_core "refine") in
- Loc.tag ?loc @@ CTacApp (refine, [thunk (of_hyp ?loc id)])
+ CAst.make ?loc @@ CTacApp (refine, [thunk (of_hyp ?loc id)])
let of_exact_var ?loc id =
let refine = global_ref ?loc (control_core "refine") in
- Loc.tag ?loc @@ CTacApp (refine, [thunk (of_variable id)])
+ CAst.make ?loc @@ CTacApp (refine, [thunk (of_variable id)])
let of_dispatch tacs =
- let (loc, _) = tacs in
+ let loc = tacs.loc in
let default = function
| Some e -> thunk e
- | None -> thunk (Loc.tag ?loc @@ CTacCst (AbsKn (Tuple 0)))
+ | None -> thunk (CAst.make ?loc @@ CTacCst (AbsKn (Tuple 0)))
in
- let map e = of_pair default (fun l -> of_list ?loc default l) (Loc.tag ?loc e) in
+ let map e = of_pair default (fun l -> of_list ?loc default l) (CAst.make ?loc e) in
of_pair (fun l -> of_list ?loc default l) (fun r -> of_option ?loc map r) tacs
let make_red_flag l =
let open Genredexpr in
let rec add_flag red = function
| [] -> red
- | (_, flag) :: lf ->
+ | {v=flag} :: lf ->
let red = match flag with
| QBeta -> { red with rBeta = true }
| QMatch -> { red with rMatch = true }
| QFix -> { red with rFix = true }
| QCofix -> { red with rCofix = true }
| QZeta -> { red with rZeta = true }
- | QConst (loc, l) ->
+ | QConst {loc;v=l} ->
if red.rDelta then
CErrors.user_err ?loc Pp.(str
"Cannot set both constants to unfold and constants not to unfold");
{ red with rConst = red.rConst @ l }
- | QDeltaBut (loc, l) ->
+ | QDeltaBut {loc;v=l} ->
if red.rConst <> [] && not red.rDelta then
CErrors.user_err ?loc Pp.(str
"Cannot set both constants to unfold and constants not to unfold");
@@ -348,10 +349,10 @@ let of_reference r =
in
of_anti of_ref r
-let of_strategy_flag (loc, flag) =
+let of_strategy_flag {loc;v=flag} =
let open Genredexpr in
let flag = make_red_flag flag in
- Loc.tag ?loc @@ CTacRec ([
+ CAst.make ?loc @@ CTacRec ([
std_proj "rBeta", of_bool ?loc flag.rBeta;
std_proj "rMatch", of_bool ?loc flag.rMatch;
std_proj "rFix", of_bool ?loc flag.rFix;
@@ -361,7 +362,7 @@ let of_strategy_flag (loc, flag) =
std_proj "rConst", of_list ?loc of_reference flag.rConst;
])
-let of_hintdb (loc, hdb) = match hdb with
+let of_hintdb {loc;v=hdb} = match hdb with
| QHintAll -> of_option ?loc (fun l -> of_list (fun id -> of_anti of_ident id) l) None
| QHintDbs ids -> of_option ?loc (fun l -> of_list (fun id -> of_anti of_ident id) l) (Some ids)
@@ -375,8 +376,8 @@ let extract_name ?loc oid = match oid with
[(match_kind * pattern * (context -> constr array -> 'a))]
where the function binds the names from the pattern to the contents of the
constr array. *)
-let of_constr_matching (loc, m) =
- let map (loc, ((ploc, pat), tac)) =
+let of_constr_matching {loc;v=m} =
+ let map {loc;v=({loc=ploc;v=pat}, tac)} =
let (knd, pat, na) = match pat with
| QConstrMatchPattern pat ->
let knd = constructor ?loc (pattern_core "MatchPattern") [] in
@@ -391,7 +392,7 @@ let of_constr_matching (loc, m) =
let vars = Id.Set.elements vars in
let vars = List.map (fun id -> Name id) vars in
let e = abstract_vars loc vars tac in
- let e = Loc.tag ?loc @@ CTacFun ([Loc.tag ?loc @@ CPatVar na], e) in
+ let e = CAst.make ?loc @@ CTacFun ([CAst.make ?loc @@ CPatVar na], e) in
let pat = inj_wit ?loc:ploc wit_pattern pat in
of_tuple [knd; pat; e]
in
@@ -401,8 +402,8 @@ let of_constr_matching (loc, m) =
- a goal pattern: (constr_match list * constr_match)
- a branch function (ident array -> context array -> constr array -> context -> 'a)
*)
-let of_goal_matching (loc, gm) =
- let mk_pat (loc, p) = match p with
+let of_goal_matching {loc;v=gm} =
+ let mk_pat {loc;v=p} = match p with
| QConstrMatchPattern pat ->
let knd = constructor ?loc (pattern_core "MatchPattern") [] in
(Anonymous, pat, knd)
@@ -411,7 +412,7 @@ let of_goal_matching (loc, gm) =
let knd = constructor ?loc (pattern_core "MatchContext") [] in
(na, pat, knd)
in
- let mk_gpat (loc, p) =
+ let mk_gpat {loc;v=p} =
let concl_pat = p.q_goal_match_concl in
let hyps_pats = p.q_goal_match_hyps in
let (concl_ctx, concl_pat, concl_knd) = mk_pat concl_pat in
@@ -433,9 +434,9 @@ let of_goal_matching (loc, gm) =
let subst = List.map (fun id -> Name id) vars in
(r, hyps, hctx, subst, concl_ctx)
in
- let map (loc, (pat, tac)) =
+ let map {loc;v=(pat, tac)} =
let (pat, hyps, hctx, subst, cctx) = mk_gpat pat in
- let tac = Loc.tag ?loc @@ CTacFun ([Loc.tag ?loc @@ CPatVar cctx], tac) in
+ let tac = CAst.make ?loc @@ CTacFun ([CAst.make ?loc @@ CPatVar cctx], tac) in
let tac = abstract_vars loc subst tac in
let tac = abstract_vars loc hctx tac in
let tac = abstract_vars loc hyps tac in
@@ -443,7 +444,7 @@ let of_goal_matching (loc, gm) =
in
of_list ?loc map gm
-let of_move_location (loc, mv) = match mv with
+let of_move_location {loc;v=mv} = match mv with
| QMoveAfter id -> std_constructor ?loc "MoveAfter" [of_anti of_ident id]
| QMoveBefore id -> std_constructor ?loc "MoveBefore" [of_anti of_ident id]
| QMoveFirst -> std_constructor ?loc "MoveFirst" []
@@ -452,7 +453,7 @@ let of_move_location (loc, mv) = match mv with
let of_pose p =
of_pair (fun id -> of_option (fun id -> of_anti of_ident id) id) of_open_constr p
-let of_assertion (loc, ast) = match ast with
+let of_assertion {loc;v=ast} = match ast with
| QAssertType (ipat, c, tac) ->
let ipat = of_option of_intro_pattern ipat in
let c = of_constr c in
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index 3f6c9a55e5..94e1734222 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Loc
open Names
open Tac2dyn
open Tac2qexpr
@@ -23,15 +22,15 @@ val thunk : raw_tacexpr -> raw_tacexpr
val of_anti : ('a -> raw_tacexpr) -> 'a or_anti -> raw_tacexpr
-val of_int : int located -> raw_tacexpr
+val of_int : int CAst.t -> raw_tacexpr
-val of_pair : ('a -> raw_tacexpr) -> ('b -> raw_tacexpr) -> ('a * 'b) located -> raw_tacexpr
+val of_pair : ('a -> raw_tacexpr) -> ('b -> raw_tacexpr) -> ('a * 'b) CAst.t -> raw_tacexpr
val of_tuple : ?loc:Loc.t -> raw_tacexpr list -> raw_tacexpr
-val of_variable : Id.t located -> raw_tacexpr
+val of_variable : Id.t CAst.t -> raw_tacexpr
-val of_ident : Id.t located -> raw_tacexpr
+val of_ident : Id.t CAst.t -> raw_tacexpr
val of_constr : Constrexpr.constr_expr -> raw_tacexpr
@@ -43,7 +42,7 @@ val of_bindings : bindings -> raw_tacexpr
val of_intro_pattern : intro_pattern -> raw_tacexpr
-val of_intro_patterns : intro_pattern list located -> raw_tacexpr
+val of_intro_patterns : intro_pattern list CAst.t -> raw_tacexpr
val of_clause : clause -> raw_tacexpr
@@ -63,13 +62,13 @@ val of_move_location : move_location -> raw_tacexpr
val of_reference : Libnames.reference or_anti -> raw_tacexpr
-val of_hyp : ?loc:Loc.t -> Id.t located -> raw_tacexpr
+val of_hyp : ?loc:Loc.t -> Id.t CAst.t -> raw_tacexpr
(** id ↦ 'Control.hyp @id' *)
-val of_exact_hyp : ?loc:Loc.t -> Id.t located -> raw_tacexpr
+val of_exact_hyp : ?loc:Loc.t -> Id.t CAst.t -> raw_tacexpr
(** id ↦ 'Control.refine (fun () => Control.hyp @id') *)
-val of_exact_var : ?loc:Loc.t -> Id.t located -> raw_tacexpr
+val of_exact_var : ?loc:Loc.t -> Id.t CAst.t -> raw_tacexpr
(** id ↦ 'Control.refine (fun () => Control.hyp @id') *)
val of_dispatch : dispatch -> raw_tacexpr
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index 65cdef0f3f..9bc23e91d7 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -37,16 +37,16 @@ let delayed_of_thunk r tac env sigma =
let mk_bindings = function
| ImplicitBindings l -> Misctypes.ImplicitBindings l
| ExplicitBindings l ->
- let l = List.map Loc.tag l in
+ let l = List.map CAst.make l in
Misctypes.ExplicitBindings l
| NoBindings -> Misctypes.NoBindings
let mk_with_bindings (x, b) = (x, mk_bindings b)
let rec mk_intro_pattern = function
-| IntroForthcoming b -> Loc.tag @@ Misctypes.IntroForthcoming b
-| IntroNaming ipat -> Loc.tag @@ Misctypes.IntroNaming (mk_intro_pattern_naming ipat)
-| IntroAction ipat -> Loc.tag @@ Misctypes.IntroAction (mk_intro_pattern_action ipat)
+| IntroForthcoming b -> CAst.make @@ Misctypes.IntroForthcoming b
+| IntroNaming ipat -> CAst.make @@ Misctypes.IntroNaming (mk_intro_pattern_naming ipat)
+| IntroAction ipat -> CAst.make @@ Misctypes.IntroAction (mk_intro_pattern_action ipat)
and mk_intro_pattern_naming = function
| IntroIdentifier id -> Misctypes.IntroIdentifier id
@@ -58,7 +58,7 @@ and mk_intro_pattern_action = function
| IntroOrAndPattern ipat -> Misctypes.IntroOrAndPattern (mk_or_and_intro_pattern ipat)
| IntroInjection ipats -> Misctypes.IntroInjection (List.map mk_intro_pattern ipats)
| IntroApplyOn (c, ipat) ->
- let c = Loc.tag @@ delayed_of_thunk Tac2ffi.constr c in
+ let c = CAst.make @@ delayed_of_thunk Tac2ffi.constr c in
Misctypes.IntroApplyOn (c, mk_intro_pattern ipat)
| IntroRewrite b -> Misctypes.IntroRewrite b
@@ -94,7 +94,7 @@ let intros_patterns ev ipat =
let apply adv ev cb cl =
let map c =
let c = thaw constr_with_bindings c >>= fun p -> return (mk_with_bindings p) in
- None, Loc.tag (delayed_of_tactic c)
+ None, CAst.make (delayed_of_tactic c)
in
let cb = List.map map cb in
match cl with
@@ -111,8 +111,8 @@ let mk_destruction_arg = function
| ElimOnAnonHyp n -> Misctypes.ElimOnAnonHyp n
let mk_induction_clause (arg, eqn, as_, occ) =
- let eqn = Option.map (fun ipat -> Loc.tag @@ mk_intro_pattern_naming ipat) eqn in
- let as_ = Option.map (fun ipat -> Loc.tag @@ mk_or_and_intro_pattern ipat) as_ in
+ let eqn = Option.map (fun ipat -> CAst.make @@ mk_intro_pattern_naming ipat) eqn in
+ let as_ = Option.map (fun ipat -> CAst.make @@ mk_or_and_intro_pattern ipat) as_ in
let occ = Option.map mk_clause occ in
((None, mk_destruction_arg arg), (eqn, as_), occ)
@@ -188,7 +188,7 @@ let forward fst tac ipat c =
let assert_ = function
| AssertValue (id, c) ->
- let ipat = Loc.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id) in
+ let ipat = CAst.make @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id) in
Tactics.forward true None (Some ipat) c
| AssertType (ipat, c, tac) ->
let ipat = Option.map mk_intro_pattern ipat in
@@ -196,7 +196,7 @@ let assert_ = function
Tactics.forward true (Some tac) ipat c
let letin_pat_tac ev ipat na c cl =
- let ipat = Option.map (fun (b, ipat) -> (b, Loc.tag @@ mk_intro_pattern_naming ipat)) ipat in
+ let ipat = Option.map (fun (b, ipat) -> (b, CAst.make @@ mk_intro_pattern_naming ipat)) ipat in
let cl = mk_clause cl in
Tactics.letin_pat_tac ev ipat na c cl
@@ -420,7 +420,7 @@ let inversion knd arg pat ids =
begin match pat with
| None -> Proofview.tclUNIT None
| Some (IntroAction (IntroOrAndPattern p)) ->
- Proofview.tclUNIT (Some (Loc.tag @@ mk_or_and_intro_pattern p))
+ Proofview.tclUNIT (Some (CAst.make @@ mk_or_and_intro_pattern p))
| Some _ ->
Tacticals.New.tclZEROMSG (str "Inversion only accept disjunctive patterns")
end >>= fun pat ->
@@ -433,7 +433,7 @@ let inversion knd arg pat ids =
Inv.inv_clause knd pat ids (NamedHyp id)
| Some (_, Misctypes.ElimOnConstr c) ->
let open Misctypes in
- let anon = Loc.tag @@ IntroNaming IntroAnonymous in
+ let anon = CAst.make @@ IntroNaming IntroAnonymous in
Tactics.specialize c (Some anon) >>= fun () ->
Tacticals.New.onLastHypId (fun id -> Inv.inv_clause knd pat ids (NamedHyp id))
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 22:42:36 +0000