aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/g_ltac2.ml4125
-rw-r--r--src/tac2qexpr.mli49
-rw-r--r--src/tac2quote.ml66
-rw-r--r--src/tac2quote.mli25
4 files changed, 156 insertions, 109 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index bfef4fab8d..b10f8d66bd 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -149,12 +149,12 @@ GEXTEND Gram
| s = Prim.string -> CTacAtm (Loc.tag ~loc:!@loc (AtmStr s))
| id = Prim.qualid ->
if Tac2env.is_constructor (snd id) then CTacCst (!@loc, RelId id) else CTacRef (RelId id)
- | "@"; id = Prim.ident -> Tac2quote.of_ident ~loc:!@loc id
- | "&"; id = Prim.ident -> Tac2quote.of_hyp ~loc:!@loc id
+ | "@"; id = Prim.ident -> Tac2quote.of_ident (Loc.tag ~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 ~loc:!@loc c
- | IDENT "open_constr"; ":"; "("; c = Constr.lconstr; ")" -> inj_open_constr !@loc c
- | IDENT "ident"; ":"; "("; c = Prim.ident; ")" -> Tac2quote.of_ident ~loc:!@loc c
+ | IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> Tac2quote.of_constr c
+ | IDENT "open_constr"; ":"; "("; c = Constr.lconstr; ")" -> Tac2quote.of_open_constr c
+ | IDENT "ident"; ":"; "("; c = lident; ")" -> Tac2quote.of_ident c
| IDENT "pattern"; ":"; "("; c = Constr.lconstr_pattern; ")" -> inj_pattern !@loc c
] ]
;
@@ -296,6 +296,9 @@ GEXTEND Gram
StrSyn (toks, n, e)
] ]
;
+ lident:
+ [ [ id = Prim.ident -> Loc.tag ~loc:!@loc id ] ]
+ ;
END
(** Quotation scopes used by notations *)
@@ -306,71 +309,92 @@ let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l))
GEXTEND Gram
GLOBAL: q_ident q_bindings q_intropattern q_intropatterns q_induction_clause;
+ anti:
+ [ [ "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id) ] ]
+ ;
ident_or_anti:
- [ [ id = Prim.ident -> QExpr id
+ [ [ id = lident -> QExpr id
| "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id)
] ]
;
+ lident:
+ [ [ id = Prim.ident -> Loc.tag ~loc:!@loc id ] ]
+ ;
+ lnatural:
+ [ [ n = Prim.natural -> Loc.tag ~loc:!@loc n ] ]
+ ;
q_ident:
[ [ id = ident_or_anti -> Tac2quote.of_anti ~loc:!@loc Tac2quote.of_ident id ] ]
;
+ qhyp:
+ [ [ x = anti -> x
+ | n = lnatural -> QExpr (Loc.tag ~loc:!@loc @@ QAnonHyp n)
+ | id = lident -> QExpr (Loc.tag ~loc:!@loc @@ QNamedHyp id)
+ ] ]
+ ;
simple_binding:
- [ [ "("; "$"; id = Prim.ident; ":="; c = Constr.lconstr; ")" ->
- Loc.tag ~loc:!@loc (QAnti (Loc.tag ~loc:!@loc id), c)
- | "("; n = Prim.natural; ":="; c = Constr.lconstr; ")" ->
- Loc.tag ~loc:!@loc (QExpr (AnonHyp n), c)
- | "("; id = Prim.ident; ":="; c = Constr.lconstr; ")" ->
- Loc.tag ~loc:!@loc (QExpr (NamedHyp id), c)
+ [ [ "("; h = qhyp; ":="; c = Constr.lconstr; ")" ->
+ Loc.tag ~loc:!@loc (h, c)
] ]
;
bindings:
[ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding ->
- QExplicitBindings bl
+ Loc.tag ~loc:!@loc @@ QExplicitBindings bl
| bl = LIST1 Constr.constr ->
- QImplicitBindings bl
+ Loc.tag ~loc:!@loc @@ QImplicitBindings bl
] ]
;
q_bindings:
- [ [ "with"; bl = bindings -> Tac2quote.of_bindings ~loc:!@loc bl
- | -> Tac2quote.of_bindings ~loc:!@loc QNoBindings
- ] ]
+ [ [ bl = with_bindings -> Tac2quote.of_bindings bl ] ]
;
intropatterns:
- [ [ l = LIST0 nonsimple_intropattern -> l ]]
+ [ [ l = LIST0 nonsimple_intropattern -> Loc.tag ~loc:!@loc l ]]
;
(* ne_intropatterns: *)
(* [ [ l = LIST1 nonsimple_intropattern -> l ]] *)
(* ; *)
or_and_intropattern:
- [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> QIntroOrPattern tc
- | "()" -> QIntroAndPattern []
- | "("; si = simple_intropattern; ")" -> QIntroAndPattern [si]
+ [ [ "["; 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])
| "("; si = simple_intropattern; ",";
tc = LIST1 simple_intropattern SEP "," ; ")" ->
- QIntroAndPattern (si::tc)
+ Loc.tag ~loc:!@loc @@ QIntroAndPattern (Loc.tag ~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 -> l
- | t::q -> [t; (QIntroAction (QIntroOrAndPattern (QIntroAndPattern (pairify q))))]
- in QIntroAndPattern (pairify (si::tc)) ] ]
+ | ([]|[_]|[_;_]) as l -> Loc.tag ~loc:!@loc l
+ | t::q ->
+ let q =
+ Loc.tag ~loc:!@loc @@
+ QIntroAction (Loc.tag ~loc:!@loc @@
+ QIntroOrAndPattern (Loc.tag ~loc:!@loc @@
+ QIntroAndPattern (pairify q)))
+ in
+ Loc.tag ~loc:!@loc [t; q]
+ in Loc.tag ~loc:!@loc @@ QIntroAndPattern (pairify (si::tc)) ] ]
;
equality_intropattern:
- [ [ "->" -> QIntroRewrite true
- | "<-" -> QIntroRewrite false
- | "[="; tc = intropatterns; "]" -> QIntroInjection tc ] ]
+ [ [ "->" -> Loc.tag ~loc:!@loc @@ QIntroRewrite true
+ | "<-" -> Loc.tag ~loc:!@loc @@ QIntroRewrite false
+ | "[="; tc = intropatterns; "]" -> Loc.tag ~loc:!@loc @@ QIntroInjection tc ] ]
;
naming_intropattern:
- [ [ LEFTQMARK; id = Prim.ident -> QIntroFresh (QExpr id)
- | "?$"; id = Prim.ident -> QIntroFresh (QAnti (Loc.tag ~loc:!@loc id))
- | "?" -> QIntroAnonymous
- | id = ident_or_anti -> QIntroIdentifier id ] ]
+ [ [ LEFTQMARK; id = lident ->
+ Loc.tag ~loc:!@loc @@ QIntroFresh (QExpr id)
+ | "?$"; id = lident ->
+ Loc.tag ~loc:!@loc @@ QIntroFresh (QAnti id)
+ | "?" ->
+ Loc.tag ~loc:!@loc @@ QIntroAnonymous
+ | id = ident_or_anti ->
+ Loc.tag ~loc:!@loc @@ QIntroIdentifier id
+ ] ]
;
nonsimple_intropattern:
[ [ l = simple_intropattern -> l
- | "*" -> QIntroForthcoming true
- | "**" -> QIntroForthcoming false ]]
+ | "*" -> Loc.tag ~loc:!@loc @@ QIntroForthcoming true
+ | "**" -> Loc.tag ~loc:!@loc @@ QIntroForthcoming false ]]
;
simple_intropattern:
[ [ pat = simple_intropattern_closed ->
@@ -380,19 +404,24 @@ GEXTEND Gram
] ]
;
simple_intropattern_closed:
- [ [ pat = or_and_intropattern -> QIntroAction (QIntroOrAndPattern pat)
- | pat = equality_intropattern -> QIntroAction pat
- | "_" -> QIntroAction QIntroWildcard
- | pat = naming_intropattern -> QIntroNaming pat ] ]
+ [ [ pat = or_and_intropattern ->
+ Loc.tag ~loc:!@loc @@ QIntroAction (Loc.tag ~loc:!@loc @@ QIntroOrAndPattern pat)
+ | pat = equality_intropattern ->
+ Loc.tag ~loc:!@loc @@ QIntroAction pat
+ | "_" ->
+ Loc.tag ~loc:!@loc @@ QIntroAction (Loc.tag ~loc:!@loc @@ QIntroWildcard)
+ | pat = naming_intropattern ->
+ Loc.tag ~loc:!@loc @@ QIntroNaming pat
+ ] ]
;
q_intropatterns:
- [ [ ipat = intropatterns -> Tac2quote.of_intro_patterns ~loc:!@loc ipat ] ]
+ [ [ ipat = intropatterns -> Tac2quote.of_intro_patterns ipat ] ]
;
q_intropattern:
- [ [ ipat = simple_intropattern -> Tac2quote.of_intro_pattern ~loc:!@loc ipat ] ]
+ [ [ ipat = simple_intropattern -> Tac2quote.of_intro_pattern ipat ] ]
;
nat_or_anti:
- [ [ n = Prim.natural -> QExpr n
+ [ [ n = lnatural -> QExpr n
| "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id)
] ]
;
@@ -402,14 +431,14 @@ GEXTEND Gram
] ]
;
with_bindings:
- [ [ "with"; bl = bindings -> bl | -> QNoBindings ] ]
+ [ [ "with"; bl = bindings -> bl | -> Loc.tag ~loc:!@loc @@ QNoBindings ] ]
;
constr_with_bindings:
- [ [ c = Constr.constr; l = with_bindings -> (c, l) ] ]
+ [ [ c = Constr.constr; l = with_bindings -> Loc.tag ~loc:!@loc @@ (c, l) ] ]
;
destruction_arg:
- [ [ n = Prim.natural -> QElimOnAnonHyp n
- | (c, bnd) = constr_with_bindings -> QElimOnConstr (c, bnd)
+ [ [ n = lnatural -> QElimOnAnonHyp n
+ | c = constr_with_bindings -> QElimOnConstr c
] ]
;
as_or_and_ipat:
@@ -463,7 +492,7 @@ GEXTEND Gram
induction_clause:
[ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat;
cl = opt_clause ->
- {
+ Loc.tag ~loc:!@loc @@ {
indcl_arg = c;
indcl_eqn = eq;
indcl_as = pat;
@@ -472,7 +501,7 @@ GEXTEND Gram
] ]
;
q_induction_clause:
- [ [ cl = induction_clause -> Tac2quote.of_induction_clause ~loc:!@loc cl ] ]
+ [ [ cl = induction_clause -> Tac2quote.of_induction_clause cl ] ]
;
END
@@ -483,7 +512,7 @@ GEXTEND Gram
[ [ IDENT "ltac2"; ":"; "("; tac = tac2expr; ")" ->
let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
CAst.make ~loc:!@loc (CHole (None, IntroAnonymous, Some arg))
- | "&"; id = Prim.ident ->
+ | "&"; id = [ id = Prim.ident -> Loc.tag ~loc:!@loc id ] ->
let tac = Tac2quote.of_exact_hyp ~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))
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index 8a61590a1d..0eb9e9f4b5 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -18,48 +18,61 @@ type 'a or_anti =
| QExpr of 'a
| QAnti of Id.t located
-type bindings =
+type quantified_hypothesis =
+| QAnonHyp of int located
+| QNamedHyp of Id.t located
+
+type bindings_r =
| QImplicitBindings of Constrexpr.constr_expr list
-| QExplicitBindings of (Misctypes.quantified_hypothesis or_anti * Constrexpr.constr_expr) Loc.located list
+| QExplicitBindings of (quantified_hypothesis located or_anti * Constrexpr.constr_expr) located list
| QNoBindings
-type intro_pattern =
+type bindings = bindings_r located
+
+type intro_pattern_r =
| QIntroForthcoming of bool
| QIntroNaming of intro_pattern_naming
| QIntroAction of intro_pattern_action
-and intro_pattern_naming =
-| QIntroIdentifier of Id.t or_anti
-| QIntroFresh of Id.t or_anti
+and intro_pattern_naming_r =
+| QIntroIdentifier of Id.t located or_anti
+| QIntroFresh of Id.t located or_anti
| QIntroAnonymous
-and intro_pattern_action =
+and intro_pattern_action_r =
| QIntroWildcard
| QIntroOrAndPattern of or_and_intro_pattern
-| QIntroInjection of intro_pattern list
+| QIntroInjection of intro_pattern list located
(* | QIntroApplyOn of Empty.t (** Not implemented yet *) *)
| QIntroRewrite of bool
-and or_and_intro_pattern =
-| QIntroOrPattern of intro_pattern list list
-| QIntroAndPattern of intro_pattern list
+and or_and_intro_pattern_r =
+| QIntroOrPattern of intro_pattern list located list
+| QIntroAndPattern of intro_pattern list located
+
+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
type occurrences =
| QAllOccurrences
-| QAllOccurrencesBut of int or_anti list
+| QAllOccurrencesBut of int located or_anti list
| QNoOccurrences
-| QOnlyOccurrences of int or_anti list
+| QOnlyOccurrences of int located or_anti list
-type hyp_location = (occurrences * Id.t or_anti) * Locus.hyp_location_flag
+type hyp_location = (occurrences * Id.t located or_anti) * Locus.hyp_location_flag
type clause =
{ q_onhyps : hyp_location list option; q_concl_occs : occurrences; }
type destruction_arg =
-| QElimOnConstr of Constrexpr.constr_expr * bindings
-| QElimOnIdent of Id.t
-| QElimOnAnonHyp of int
+| QElimOnConstr of (Constrexpr.constr_expr * bindings) located
+| QElimOnIdent of Id.t located
+| QElimOnAnonHyp of int located
-type induction_clause = {
+type induction_clause_r = {
indcl_arg : destruction_arg;
indcl_eqn : intro_pattern_naming option;
indcl_as : or_and_intro_pattern option;
indcl_in : clause option;
}
+
+type induction_clause = induction_clause_r located
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index a053bd799f..1cba488768 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -54,7 +54,7 @@ let of_tuple ?loc el =
let len = List.length el in
CTacApp (loc, CTacCst (loc, AbsKn (Tuple len)), el)
-let of_int ?loc n =
+let of_int (loc, n) =
CTacAtm (Loc.tag ?loc (AtmInt n))
let of_option ?loc opt = match opt with
@@ -65,21 +65,25 @@ let inj_wit ?loc wit x =
let loc = Option.default dummy_loc loc in
CTacExt (loc, Genarg.in_gen (Genarg.rawwit wit) x)
-let of_variable ?loc id =
+let of_variable (loc, id) =
let qid = Libnames.qualid_of_ident id in
if Tac2env.is_constructor qid then
CErrors.user_err ?loc (str "Invalid identifier")
else CTacRef (RelId (Loc.tag ?loc qid))
let of_anti ?loc f = function
-| QExpr x -> f ?loc x
-| QAnti (loc, id) -> of_variable ?loc id
+| QExpr x -> f x
+| QAnti id -> of_variable id
-let of_ident ?loc id = inj_wit ?loc Stdarg.wit_ident id
+let of_ident (loc, id) = inj_wit ?loc Stdarg.wit_ident id
-let of_constr ?loc c = inj_wit ?loc Stdarg.wit_constr c
+let of_constr c =
+ let loc = Constrexpr_ops.constr_loc c in
+ inj_wit ?loc Stdarg.wit_constr c
-let of_open_constr ?loc c = inj_wit ?loc Stdarg.wit_open_constr c
+let of_open_constr c =
+ let loc = Constrexpr_ops.constr_loc c in
+ inj_wit ?loc Stdarg.wit_open_constr c
let of_bool ?loc b =
let c = if b then Core.c_true else Core.c_false in
@@ -90,22 +94,22 @@ let rec of_list ?loc = function
| e :: l ->
constructor ?loc Core.c_cons [e; of_list ?loc l]
-let of_qhyp ?loc = function
-| AnonHyp n -> constructor Core.c_anon_hyp [of_int ?loc n]
-| NamedHyp id -> constructor Core.c_named_hyp [of_ident ?loc id]
+let of_qhyp (loc, h) = match h with
+| QAnonHyp n -> constructor ?loc Core.c_anon_hyp [of_int n]
+| QNamedHyp id -> constructor ?loc Core.c_named_hyp [of_ident id]
-let of_bindings ?loc = function
+let of_bindings (loc, b) = match b with
| QNoBindings ->
std_constructor ?loc "NoBindings" []
| QImplicitBindings tl ->
- let tl = List.map (fun c -> of_open_constr ?loc c) tl in
+ let tl = List.map of_open_constr tl in
std_constructor ?loc "ImplicitBindings" [of_list ?loc tl]
| QExplicitBindings tl ->
- let map (loc, (qhyp, e)) = of_pair ?loc (of_anti ?loc of_qhyp qhyp, of_open_constr ?loc e) in
+ let map (loc, (qhyp, e)) = of_pair ?loc (of_anti ?loc of_qhyp qhyp, of_open_constr e) in
let tl = List.map map tl in
std_constructor ?loc "ExplicitBindings" [of_list ?loc tl]
-let rec of_intro_pattern ?loc = function
+let rec of_intro_pattern (loc, pat) = match pat with
| QIntroForthcoming b ->
std_constructor ?loc "IntroForthcoming" [of_bool b]
| QIntroNaming iname ->
@@ -113,33 +117,33 @@ let rec of_intro_pattern ?loc = function
| QIntroAction iact ->
std_constructor ?loc "IntroAction" [of_intro_pattern_action iact]
-and of_intro_pattern_naming ?loc = function
+and of_intro_pattern_naming (loc, pat) = match pat with
| QIntroIdentifier id ->
- std_constructor ?loc "IntroIdentifier" [of_anti ?loc of_ident id]
+ std_constructor ?loc "IntroIdentifier" [of_anti of_ident id]
| QIntroFresh id ->
std_constructor ?loc "IntroFresh" [of_anti ?loc of_ident id]
| QIntroAnonymous ->
std_constructor ?loc "IntroAnonymous" []
-and of_intro_pattern_action ?loc = function
+and of_intro_pattern_action (loc, pat) = match pat with
| QIntroWildcard ->
std_constructor ?loc "IntroWildcard" []
| QIntroOrAndPattern pat ->
- std_constructor ?loc "IntroOrAndPattern" [of_or_and_intro_pattern ?loc pat]
+ std_constructor ?loc "IntroOrAndPattern" [of_or_and_intro_pattern pat]
| QIntroInjection il ->
- std_constructor ?loc "IntroInjection" [of_intro_patterns ?loc il]
+ std_constructor ?loc "IntroInjection" [of_intro_patterns il]
| QIntroRewrite b ->
std_constructor ?loc "IntroRewrite" [of_bool ?loc b]
-and of_or_and_intro_pattern ?loc = function
+and of_or_and_intro_pattern (loc, pat) = match pat with
| QIntroOrPattern ill ->
- let ill = List.map (of_intro_patterns ?loc) ill in
+ let ill = List.map of_intro_patterns ill in
std_constructor ?loc "IntroOrPattern" [of_list ?loc ill]
| QIntroAndPattern il ->
- std_constructor ?loc "IntroAndPattern" [of_intro_patterns ?loc il]
+ std_constructor ?loc "IntroAndPattern" [of_intro_patterns il]
-and of_intro_patterns ?loc l =
- of_list ?loc (List.map (of_intro_pattern ?loc) l)
+and of_intro_patterns (loc, l) =
+ of_list ?loc (List.map of_intro_pattern l)
let of_hyp_location_flag ?loc = function
| Locus.InHyp -> std_constructor ?loc "InHyp" []
@@ -175,15 +179,15 @@ let of_clause ?loc cl =
])
let of_destruction_arg ?loc = function
-| QElimOnConstr (c, bnd) ->
- let c = of_open_constr ?loc c in
- let bnd = of_bindings ?loc bnd in
+| QElimOnConstr (loc, (c, bnd)) ->
+ let c = of_open_constr c in
+ let bnd = of_bindings bnd in
let arg = thunk (of_pair ?loc (c, bnd)) in
std_constructor ?loc "ElimOnConstr" [arg]
-| QElimOnIdent id -> std_constructor ?loc "ElimOnIdent" [of_ident ?loc id]
-| QElimOnAnonHyp n -> std_constructor ?loc "ElimOnAnonHyp" [of_int ?loc n]
+| 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, cl) =
let arg = of_destruction_arg ?loc cl.indcl_arg in
let eqn = of_option ?loc (Option.map of_intro_pattern_naming cl.indcl_eqn) in
let as_ = of_option ?loc (Option.map of_or_and_intro_pattern cl.indcl_as) in
@@ -199,7 +203,7 @@ let of_induction_clause ?loc cl =
let of_hyp ?loc id =
let loc = Option.default dummy_loc loc in
let hyp = CTacRef (AbsKn (control_core "hyp")) in
- CTacApp (loc, hyp, [of_ident ~loc id])
+ CTacApp (loc, hyp, [of_ident id])
let of_exact_hyp ?loc id =
let loc = Option.default dummy_loc loc in
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index 40ea58e334..404e9378e0 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Loc
open Names
open Misctypes
open Tac2qexpr
@@ -18,32 +19,32 @@ open Tac2expr
val constructor : ?loc:Loc.t -> ltac_constructor -> raw_tacexpr list -> raw_tacexpr
-val of_anti : ?loc:Loc.t -> (?loc:Loc.t -> 'a -> raw_tacexpr) -> 'a or_anti -> raw_tacexpr
+val of_anti : ?loc:Loc.t -> ('a -> raw_tacexpr) -> 'a or_anti -> raw_tacexpr
-val of_int : ?loc:Loc.t -> int -> raw_tacexpr
+val of_int : int located -> raw_tacexpr
val of_pair : ?loc:Loc.t -> raw_tacexpr * raw_tacexpr -> raw_tacexpr
-val of_variable : ?loc:Loc.t -> Id.t -> raw_tacexpr
+val of_variable : Id.t located -> raw_tacexpr
-val of_ident : ?loc:Loc.t -> Id.t -> raw_tacexpr
+val of_ident : Id.t located -> raw_tacexpr
-val of_constr : ?loc:Loc.t -> Constrexpr.constr_expr -> raw_tacexpr
+val of_constr : Constrexpr.constr_expr -> raw_tacexpr
-val of_open_constr : ?loc:Loc.t -> Constrexpr.constr_expr -> raw_tacexpr
+val of_open_constr : Constrexpr.constr_expr -> raw_tacexpr
val of_list : ?loc:Loc.t -> raw_tacexpr list -> raw_tacexpr
-val of_bindings : ?loc:Loc.t -> bindings -> raw_tacexpr
+val of_bindings : bindings -> raw_tacexpr
-val of_intro_pattern : ?loc:Loc.t -> intro_pattern -> raw_tacexpr
+val of_intro_pattern : intro_pattern -> raw_tacexpr
-val of_intro_patterns : ?loc:Loc.t -> intro_pattern list -> raw_tacexpr
+val of_intro_patterns : intro_pattern list located -> raw_tacexpr
-val of_induction_clause : ?loc:Loc.t -> induction_clause -> raw_tacexpr
+val of_induction_clause : induction_clause -> raw_tacexpr
-val of_hyp : ?loc:Loc.t -> Id.t -> raw_tacexpr
+val of_hyp : ?loc:Loc.t -> Id.t located -> raw_tacexpr
(** id ↦ 'Control.hyp @id' *)
-val of_exact_hyp : ?loc:Loc.t -> Id.t -> raw_tacexpr
+val of_exact_hyp : ?loc:Loc.t -> Id.t located -> raw_tacexpr
(** id ↦ 'Control.refine (fun () => Control.hyp @id') *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 07:24:13 +0000