 that variable."
   (interactive)
   (if (region-active-p)
-      (fstar--destruct-match-var-1 (region-beginning) (region-end) (fstar--read-type-name))
+      (let ((type (fstar--read-type-name)))
+        (fstar--destruct-match-var-1 (region-beginning) (region-end) type type))
     (or (fstar--destruct-match-var-at-point)
         (funcall-interactively #'fstar-insert-match (fstar--read-type-name)))))
 

;;;; Insert a match

(defun fstar--split-match-var-annot (str)
  "Split var name and <<<>>> type annotation in STR."
  (save-match-data
    (if (string-match "\\(.+?\\)<<<\\(.+?\\)>>>" str)
        (let ((var (match-string 1 str))
              (type (match-string 2 str)))
          (cons var type))
      (cons str nil))))

(defun fstar--prepare-match-snippet (snippet)

(defun fstar--destruct-var-continuation (from to type response)
  "Replace FROM..TO (with TYPE) with match from RESPONSE."
  (pcase (and response (split-string response "\n"))
    (`nil
     (message "No match found for type `%s'." type))
    (`(,_name ,branch)
     (remove-text-properties from to '(fstar--match-var-type nil))
     (let ((yas-indent-line nil)
           (snip (fstar--prepare-match-snippet branch)))
       (fstar--expand-snippet snip from to)))
    (_
     (message "Can't destruct `%s' in place (it has more than one constructor)" type))))

(defun fstar--destruct-match-var-1 (from to type closed-type)
  "Replace FROM..TO by pattern matching on TYPE/CLOSED-TYPE.
TYPE is for display (tuple2 a int); CLOSED-TYPE is reparseable by
F* (fun a -> (tuple2 a int))."
  (fstar-subp--ensure-available #'user-error 'match)
  (fstar-subp--query
   (fstar-subp--show-match-query closed-type)
   (fstar-subp--pos-check-wrapper (point)
     (apply-partially #'fstar--destruct-var-continuation from to type))))

(defun fstar--destruct-match-var-at-point ()
  "Destruct match variable inserted with `fstar-insert-match'."
  (pcase (fstar--property-range (point) 'fstar--match-var-type)
    (`(,from ,to (,type . ,closed-type))
     (fstar--destruct-match-var-1 from to type closed-type)
     t)))

(defun fstar-insert-match-dwim ()
