diff options
| author | Arnaud Spiwack | 2014-02-25 20:08:00 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-02-25 20:08:00 +0100 |
| commit | e4c81a456ed7279e255e0df2a73e14c77946be7e (patch) | |
| tree | ca303727da741377b06b51a946eb4b27cbd20700 | |
| parent | 2eaf2b1093c08304d34ba898d38343f20e7538e3 (diff) | |
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.
| -rw-r--r-- | tactics/tacinterp.ml | 11 |
1 files changed, 0 insertions, 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 -> |