diff options
| -rw-r--r-- | src/g_ltac2.ml4 | 8 | ||||
| -rw-r--r-- | src/tac2core.ml | 7 | ||||
| -rw-r--r-- | src/tac2entries.mli | 2 | ||||
| -rw-r--r-- | src/tac2qexpr.mli | 10 | ||||
| -rw-r--r-- | src/tac2quote.mli | 4 |
5 files changed, 19 insertions, 12 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4 index b59a5e184e..b13c036549 100644 --- a/src/g_ltac2.ml4 +++ b/src/g_ltac2.ml4 @@ -371,8 +371,8 @@ GEXTEND Gram [ [ id = Prim.ident -> CAst.make ~loc:!@loc id ] ] ; globref: - [ [ "&"; id = Prim.ident -> CAst.make ~loc:!@loc (Libnames.Ident id) - | qid = Prim.qualid -> CAst.map (fun qid -> Libnames.Qualid qid) qid + [ [ "&"; id = Prim.ident -> CAst.make ~loc:!@loc (QHypothesis id) + | qid = Prim.qualid -> CAst.map (fun qid -> QReference qid) qid ] ] ; END @@ -666,8 +666,8 @@ GEXTEND Gram ] ] ; refglobal: - [ [ "&"; id = Prim.ident -> QExpr (CAst.make ~loc:!@loc @@ Libnames.Ident id) - | qid = Prim.qualid -> QExpr (CAst.make ~loc:!@loc @@ Libnames.Qualid qid.CAst.v) + [ [ "&"; id = Prim.ident -> QExpr (CAst.make ~loc:!@loc @@ QHypothesis id) + | qid = Prim.qualid -> QExpr (CAst.make ~loc:!@loc @@ QReference qid.CAst.v) | "$"; id = Prim.ident -> QAnti (CAst.make ~loc:!@loc id) ] ] ; diff --git a/src/tac2core.ml b/src/tac2core.ml index 5f33374486..4bd294d4df 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -910,13 +910,14 @@ let () = define_ml_object Tac2quote.wit_pattern obj let () = - let intern self ist qid = match qid with - | {CAst.v=Libnames.Ident id} -> + let intern self ist ref = match ref.CAst.v with + | Tac2qexpr.QHypothesis id -> GlbVal (Globnames.VarRef id), gtypref t_reference - | {CAst.loc;v=Libnames.Qualid qid} -> + | Tac2qexpr.QReference qid -> let gr = try Nametab.locate qid with Not_found -> + let loc = ref.CAst.loc in Nametab.error_global_not_found (CAst.make ?loc qid) in GlbVal gr, gtypref t_reference diff --git a/src/tac2entries.mli b/src/tac2entries.mli index ad7624b7d0..777f3f1a43 100644 --- a/src/tac2entries.mli +++ b/src/tac2entries.mli @@ -74,7 +74,7 @@ val q_rewriting : rewriting Pcoq.Gram.entry val q_clause : clause Pcoq.Gram.entry val q_dispatch : dispatch Pcoq.Gram.entry val q_occurrences : occurrences Pcoq.Gram.entry -val q_reference : Libnames.reference or_anti Pcoq.Gram.entry +val q_reference : reference or_anti Pcoq.Gram.entry val q_strategy_flag : strategy_flag Pcoq.Gram.entry val q_constr_matching : constr_matching Pcoq.Gram.entry val q_goal_matching : goal_matching Pcoq.Gram.entry diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli index 3f0c591e63..400ab1a092 100644 --- a/src/tac2qexpr.mli +++ b/src/tac2qexpr.mli @@ -16,6 +16,12 @@ type 'a or_anti = | QExpr of 'a | QAnti of Id.t CAst.t +type reference_r = +| QReference of Libnames.qualid +| QHypothesis of Id.t + +type reference = reference_r CAst.t + type quantified_hypothesis = | QAnonHyp of int CAst.t | QNamedHyp of Id.t CAst.t @@ -116,8 +122,8 @@ type red_flag_r = | QFix | QCofix | QZeta -| QConst of Libnames.reference or_anti list CAst.t -| QDeltaBut of Libnames.reference or_anti list CAst.t +| QConst of reference or_anti list CAst.t +| QDeltaBut of reference or_anti list CAst.t type red_flag = red_flag_r CAst.t diff --git a/src/tac2quote.mli b/src/tac2quote.mli index cc58144901..2ce347f397 100644 --- a/src/tac2quote.mli +++ b/src/tac2quote.mli @@ -60,7 +60,7 @@ val of_hintdb : hintdb -> raw_tacexpr val of_move_location : move_location -> raw_tacexpr -val of_reference : Libnames.reference or_anti -> raw_tacexpr +val of_reference : reference or_anti -> raw_tacexpr val of_hyp : ?loc:Loc.t -> Id.t CAst.t -> raw_tacexpr (** id ↦ 'Control.hyp @id' *) @@ -89,7 +89,7 @@ val wit_pattern : (Constrexpr.constr_expr, Pattern.constr_pattern) Arg.tag val wit_ident : (Id.t, Id.t) Arg.tag -val wit_reference : (Libnames.reference, GlobRef.t) Arg.tag +val wit_reference : (reference, GlobRef.t) Arg.tag (** Beware, at the raw level, [Qualid [id]] has not the same meaning as [Ident id]. The first is an unqualified global reference, the second is the dynamic reference to id. *) |