From 52247f50fa9aed83cc4a9a714b6b8f779479fd9b Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 29 Jul 2014 12:20:54 +0200
Subject: 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.
---
 intf/tacexpr.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 1375552c32..99e151e381 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -174,6 +174,10 @@ and ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_arg =
   | TacGeneric     of 'lev generic_argument
   | MetaIdArg      of Loc.t * bool * string
   | ConstrMayEval  of ('trm,'cst,'pat) may_eval
+  | UConstr        of 'trm  (* We can reuse ['trm] because terms and untyped terms
+                               only differ at interpretation time (and not at
+                               internalisation), and the output of interpration
+                               is not a variant of [tactic_expr]. *)
   | Reference      of 'ref
   | TacCall of Loc.t * 'ref *
       ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_arg list
-- 
cgit v1.2.3