diff options
| author | Arnaud Spiwack | 2014-07-29 12:20:54 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-07-29 17:16:29 +0200 |
| commit | 52247f50fa9aed83cc4a9a714b6b8f779479fd9b (patch) | |
| tree | deba7d80c23fcef9ac3632beca3b0e0b7b8567bd /printing | |
| parent | dfb5897b99cd21934c5d096c329585367665b986 (diff) | |
Add a type of untyped term to Ltac's value.
It is meant to avoid intermediary retyping when a term is built in Ltac. See #3218.
The implementation makes a small modification in Constrintern: now the main internalisation function can take an extra substitution from Ltac variables to glob_constr and will apply the substitution during the internalisation.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/pptactic.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 381534d6da..7fc214304f 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -938,6 +938,7 @@ and pr_tacarg = function | MetaIdArg (loc,false,s) -> pr_with_comments loc (str ("constr: $" ^ s)) | Reference r -> pr_ref r | ConstrMayEval c -> pr_may_eval pr_constr pr_lconstr pr_cst pr_pat c + | UConstr c -> str"uconstr:" ++ pr_constr c | TacFreshId l -> str "fresh" ++ pr_fresh_ids l | TacExternal (_,com,req,la) -> str "external" ++ spc() ++ qs com ++ spc() ++ qs req ++ |