Revert the change in Constrintern introduced by "Add a type of untyped term to Ltac's value."

It was commit 52247f50fa9aed83cc4a9a714b6b8f779479fd9b.

The closure in uconstr renders these changes (pertaining to substitution of ltac variables during internalisation) obsolete.

4 files changed, 0 insertions, 11 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index fb232762cd..6ae5ca352b 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -69,7 +69,6 @@ type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr)
 type ltac_sign = {
   ltac_vars : Id.Set.t;
   ltac_bound : Id.Set.t;
-  ltac_subst : glob_constr Lazy.t Id.Map.t;
 }
 
 let interning_grammar = ref false
@@ -657,9 +656,6 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
   if Id.Set.mem id genv.ids || Id.Set.mem id ltacvars.ltac_vars
   then
     GVar (loc,id), [], [], []
-  (* Is [id] bound to a glob_constr in the the ltac context *)
-  else if Id.Map.mem id ltacvars.ltac_subst then
-    Lazy.force (Id.Map.find id ltacvars.ltac_subst), [], [], []
   (* Is [id] a notation variable *)
   else if Id.Map.mem id ntnvars
   then
@@ -1784,7 +1780,6 @@ let scope_of_type_kind = function
 let empty_ltac_sign = {
   ltac_vars = Id.Set.empty;
   ltac_bound = Id.Set.empty;
-  ltac_subst = Id.Map.empty;
 }
 
 let intern_gen kind env
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index b6cae349d5..b5cad5d284 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -72,8 +72,6 @@ type ltac_sign = {
   (** Variables of Ltac which may be bound to a term *)
   ltac_bound : Id.Set.t;
   (** Other variables of Ltac *)
-  ltac_subst : glob_constr Lazy.t Id.Map.t;
-  (** Substitution for untyped terms *)
 }
 
 val empty_ltac_sign : ltac_sign
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 60bc784f1f..62f7d4d653 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -248,7 +248,6 @@ let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env} c =
   let ltacvars = {
     Constrintern.ltac_vars = lfun;
     ltac_bound = Id.Set.empty;
-    ltac_subst = Id.Map.empty;
   } in
   let c' =
     warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars env) c
@@ -328,7 +327,6 @@ let intern_constr_pattern ist ~as_type ~ltacvars pc =
   let ltacvars = {
     Constrintern.ltac_vars = ltacvars;
     ltac_bound = Id.Set.empty;
-    ltac_subst = Id.Map.empty;
   } in
   let metas,pat = Constrintern.intern_constr_pattern
     ist.genv ~as_type ~ltacvars pc
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 9ec486c1c3..c346a7cd35 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -480,7 +480,6 @@ let interp_uconstr ist env = function
       let ltacvars = {
         Constrintern.ltac_vars = Id.(Set.union (Map.domain typed) (Map.domain untyped));
         ltac_bound = Id.Map.domain ist.lfun;
-        ltac_subst = Id.Map.empty;
       } in
       { closure ; term =  intern_gen WithoutTypeConstraint ~ltacvars env ce }
 
@@ -496,7 +495,6 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
       let ltacvars = {
         ltac_vars = Id.Map.domain constrvars;
         ltac_bound = Id.Map.domain ist.lfun;
-        ltac_subst = Id.Map.empty;
       } in
       intern_gen kind ~allow_patvar ~ltacvars env c
   in