diff options
| author | Pierre-Marie Pédrot | 2020-09-23 11:00:50 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-23 11:00:50 +0200 |
| commit | bb6e78ef2ca4bf0d686654fa3f66dd780f5be0ac (patch) | |
| tree | ce14f693e58487503870c53d7a186bf7ca66a1f6 /plugins/ltac/tacintern.ml | |
| parent | 23b0dbb3a0a71edd9ce2137e88b715c3e36e576f (diff) | |
| parent | fb144f860a0034103ad0470b8982639277baac1b (diff) | |
Merge PR #13028: Fixes #9716 and #13004: don't drop the qualifier of quotations at printing time
Reviewed-by: ppedrot
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 |