From e4c81a456ed7279e255e0df2a73e14c77946be7e Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 25 Feb 2014 20:08:00 +0100
Subject: Tacinterp: remove the is_value check in Ltac's let-in.

It fixes micromega. It is frankly a mystery to me why psatz ever work. The semantics of Ltac's match is still fishy.---
 tactics/tacinterp.ml | 11 -----------
 1 file changed, 11 deletions(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 678d884c5f..52fb439c31 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -107,16 +107,6 @@ let curr_debug ist = match TacStore.get ist.extra f_debug with
 | None -> DebugOff
 | Some level -> level
 
-let check_is_value v =
-  let v = Value.normalize v in
-  if has_type v (topwit wit_tacvalue) then
-    let v = to_tacvalue v in
-    match v with
-    | VRTactic -> (* These are goals produced by Match *)
-      error "Immediate match producing tactics not allowed in local definitions."
-    | _ -> ()
-  else ()
-
 (** TODO: unify printing of generic Ltac values in case of coercion failure. *)
 
 (* Displays a value *)
@@ -1222,7 +1212,6 @@ and interp_letin ist llc u gl =
   let fold ((_, id), body) acc =
     interp_tacarg ist body gl >= fun v ->
     acc >= fun acc ->
-    let () = check_is_value v in
     Proofview.tclUNIT (Id.Map.add id v acc)
   in
   List.fold_right fold llc (Proofview.tclUNIT ist.lfun) >= fun lfun ->
-- 
cgit v1.2.3