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.
---
 plugins/funind/indfun.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index e10ed49ed3..2ceda4f48c 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -132,7 +132,7 @@ let rec abstract_glob_constr c = function
 
 let interp_casted_constr_with_implicits sigma env impls c  =
   Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls
-    ~allow_patvar:false  ~ltacvars:(Id.Set.empty, Id.Set.empty) c
+    ~allow_patvar:false  ~ltacvars:(Id.Set.empty, Id.Set.empty,Id.Map.empty) c
 
 (*
    Construct a fixpoint as a Glob_term
-- 
cgit v1.2.3