diff options
| author | Hugo Herbelin | 2020-09-15 21:24:39 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-09-22 18:22:12 +0200 |
| commit | d286c3601e24afe0a681d092cbd880773872b980 (patch) | |
| tree | cad1afcff0fbfbcb3c91a82fc3cf75bdee6e73d8 /plugins/ltac/tacintern.ml | |
| parent | c3a73c5e923953efea016a81d380e58b2cccb4f9 (diff) | |
Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.
Diffstat (limited to 'plugins/ltac/tacintern.ml')
| -rw-r--r-- | plugins/ltac/tacintern.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index afa79a88db..dea216045e 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -195,7 +195,7 @@ let intern_non_tactic_reference strict ist qid = if qualid_is_ident qid && not strict then let id = qualid_basename qid in let ipat = in_gen (glbwit wit_intro_pattern) (make ?loc:qid.CAst.loc @@ IntroNaming (IntroIdentifier id)) in - TacGeneric ipat + TacGeneric (None,ipat) else (* Reference not found *) let _, info = Exninfo.capture exn in @@ -713,9 +713,9 @@ and intern_tacarg strict onlytac ist = function | TacPretype c -> TacPretype (intern_constr ist c) | TacNumgoals -> TacNumgoals | Tacexp t -> Tacexp (intern_tactic onlytac ist t) - | TacGeneric arg -> + | TacGeneric (isquot,arg) -> let arg = intern_genarg ist arg in - TacGeneric arg + TacGeneric (isquot,arg) (* Reads the rules of a Match Context or a Match *) and intern_match_rule onlytac ist ?(as_type=false) = function |