1 files changed, 49 insertions, 24 deletions

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 958a205a..596feeec 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -159,8 +159,6 @@ type branch_assumptions = {
   ba        : branch_args;       (* the branch args *)
   assums    : named_context}   (* the list of assumptions introduced *)
 
-open Misctypes
-
 let fix_empty_or_and_pattern nv l =
   (* 1- The syntax does not distinguish between "[ ]" for one clause with no
      names and "[ ]" for no clause at all *)
@@ -194,7 +192,7 @@ let check_or_and_pattern_size ?loc check_and names branchsigns =
         if not (Int.equal p p1 || Int.equal p p2) then err1 p1 p2;
         if Int.equal p p1 then
           IntroAndPattern
-            (List.extend branchsigns.(0) (CAst.make @@ IntroNaming IntroAnonymous) l)
+            (List.extend branchsigns.(0) (CAst.make @@ IntroNaming Namegen.IntroAnonymous) l)
         else
           names
       else
@@ -225,7 +223,7 @@ let compute_induction_names_gen check_and branchletsigns = function
 let compute_induction_names = compute_induction_names_gen true
 
 (* Compute the let-in signature of case analysis or standard induction scheme *)
-let compute_constructor_signatures isrec ((_,k as ity),u) =
+let compute_constructor_signatures ~rec_flag ((_,k as ity),u) =
   let rec analrec c recargs =
     match Constr.kind c, recargs with
     | Prod (_,_,c), recarg::rest ->
@@ -233,7 +231,7 @@ let compute_constructor_signatures isrec ((_,k as ity),u) =
         begin match Declareops.dest_recarg recarg with
         | Norec | Imbr _  -> true :: rest
         | Mrec (_,j)  ->
-            if isrec && Int.equal j k then true :: true :: rest
+            if rec_flag && Int.equal j k then true :: true :: rest
             else true :: rest
         end
     | LetIn (_,_,_,c), rest -> false :: analrec c rest
@@ -263,7 +261,7 @@ let pf_with_evars glsev k gls =
     tclTHEN (Refiner.tclEVARS evd) (k a) gls
 
 let pf_constr_of_global gr k =
-  pf_with_evars (fun gls -> on_snd EConstr.of_constr (pf_apply Evd.fresh_global gls gr)) k
+  pf_with_evars (fun gls -> pf_apply Evd.fresh_global gls gr) k
 
 (** Tacticals of Ltac defined directly in term of Proofview *)
 module New = struct
@@ -369,9 +367,36 @@ module New = struct
     tclTHENSFIRSTn t1 l (tclUNIT())
   let tclTHENFIRST t1 t2 =
     tclTHENFIRSTn t1 [|t2|]
+
+  let tclBINDFIRST t1 t2 =
+    t1 >>= fun ans ->
+    Proofview.Unsafe.tclGETGOALS >>= fun gls ->
+    match gls with
+    | [] -> tclFAIL 0 (str "Expect at least one goal.")
+    | hd::tl ->
+    Proofview.Unsafe.tclSETGOALS [hd] <*> t2 ans >>= fun ans ->
+    Proofview.Unsafe.tclNEWGOALS tl <*>
+    Proofview.tclUNIT ans
+
   let tclTHENLASTn t1 l =
     tclTHENS3PARTS t1 [||] (tclUNIT()) l
   let tclTHENLAST t1 t2 = tclTHENLASTn t1 [|t2|]
+
+  let option_of_failure f x = try Some (f x) with Failure _ -> None
+
+  let tclBINDLAST t1 t2 =
+    t1 >>= fun ans ->
+    Proofview.Unsafe.tclGETGOALS >>= fun gls ->
+    match option_of_failure List.sep_last gls with
+    | None -> tclFAIL 0 (str "Expect at least one goal.")
+    | Some (last,firstn) ->
+    Proofview.Unsafe.tclSETGOALS [last] <*> t2 ans >>= fun ans ->
+    Proofview.Unsafe.tclGETGOALS >>= fun newgls ->
+    tclEVARMAP >>= fun sigma ->
+    let firstn = Proofview.Unsafe.undefined sigma firstn in
+    Proofview.Unsafe.tclSETGOALS (firstn@newgls) <*>
+    Proofview.tclUNIT ans
+
   let tclTHENS t l =
     tclINDEPENDENT begin
       t <*>Proofview.tclORELSE (* converts the [SizeMismatch] error into an ltac error *)
@@ -465,11 +490,13 @@ module New = struct
     Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t)
 
   (* Select a subset of the goals *)
-  let tclSELECT = function
-    | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i
-    | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l
-    | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id
-    | Vernacexpr.SelectAll -> fun tac -> tac
+  let tclSELECT = let open Goal_select in function
+    | SelectNth i -> Proofview.tclFOCUS i i
+    | SelectList l -> Proofview.tclFOCUSLIST l
+    | SelectId id -> Proofview.tclFOCUSID id
+    | SelectAll -> anomaly ~label:"tclSELECT" Pp.(str "SelectAll not allowed here")
+    | SelectAlreadyFocused ->
+      anomaly ~label:"tclSELECT" Pp.(str "SelectAlreadyFocused not allowed here")
 
   (* Check that holes in arguments have been resolved *)
 
@@ -479,8 +506,8 @@ module New = struct
       let evi = Evd.find sigma evk in
       match Evd.evar_body evi with
       | Evd.Evar_empty -> Some (evk,evi)
-      | Evd.Evar_defined c -> match Constr.kind c with
-        | Term.Evar (evk,l) -> is_undefined_up_to_restriction sigma evk
+      | Evd.Evar_defined c -> match Constr.kind (EConstr.Unsafe.to_constr c) with
+        | Evar (evk,l) -> is_undefined_up_to_restriction sigma evk
         | _ -> 
           (* We make the assumption that there is no way to refine an
             evar remaining after typing from the initial term given to
@@ -607,7 +634,7 @@ module New = struct
   (* Find the right elimination suffix corresponding to the sort of the goal *)
   (* c should be of type A1->.. An->B with B an inductive definition *)
   let general_elim_then_using mk_elim
-      isrec allnames tac predicate ind (c, t) =
+      rec_flag allnames tac predicate ind (c, t) =
     Proofview.Goal.enter begin fun gl ->
     let sigma, elim = mk_elim ind gl in
     let ind = on_snd (fun u -> EInstance.kind sigma u) ind in
@@ -628,15 +655,14 @@ module New = struct
       | _ ->
 	  let name_elim =
 	    match EConstr.kind sigma elim with
-	    | Const (kn, _) -> Constant.to_string kn
-	    | Var id -> Id.to_string id
-	    | _ -> "\b"
+            | Const _ | Var _ -> str " " ++ Printer.pr_econstr_env (pf_env gl) sigma elim
+            | _ -> mt ()
 	  in
 	  user_err ~hdr:"Tacticals.general_elim_then_using"
-            (str "The elimination combinator " ++ str name_elim ++ str " is unknown.")
+            (str "The elimination combinator " ++ name_elim ++ str " is unknown.")
     in
     let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in
-    let branchsigns = compute_constructor_signatures isrec ind in
+    let branchsigns = compute_constructor_signatures ~rec_flag ind in
     let brnames = compute_induction_names_gen false branchsigns allnames in
     let flags = Unification.elim_flags () in
     let elimclause' =
@@ -659,7 +685,7 @@ module New = struct
     in
     let branchtacs = List.init (Array.length branchsigns) after_tac in
     Proofview.tclTHEN
-      (Clenvtac.clenv_refine false clenv')
+      (Clenvtac.clenv_refine clenv')
       (Proofview.tclEXTEND [] tclIDTAC branchtacs)
     end) end
 
@@ -682,7 +708,7 @@ module New = struct
   let gl_make_elim ind = begin fun gl ->
     let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in
     let (sigma, c) = pf_apply Evd.fresh_global gl gr in
-    (sigma, EConstr.of_constr c)
+    (sigma, c)
   end
 
   let gl_make_case_dep (ind, u) = begin fun gl ->
@@ -726,8 +752,8 @@ module New = struct
     let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in
     let isrec,mkelim =
       match (Global.lookup_mind (fst (fst ind))).mind_record with
-      | None -> true,gl_make_elim
-      | Some _ -> false,gl_make_case_dep
+      | NotRecord -> true,gl_make_elim
+      | FakeRecord | PrimRecord _ -> false,gl_make_case_dep
     in
     general_elim_then_using mkelim isrec None tac None ind (c, t)
     end
@@ -742,7 +768,6 @@ module New = struct
     Proofview.tclEVARMAP >>= fun sigma ->
     Proofview.tclENV >>= fun env ->
     let (sigma, c) = Evd.fresh_global env sigma ref in
-    let c = EConstr.of_constr c in
     Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT c
 
 end