1 files changed, 171 insertions, 151 deletions

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 66da9ee1..958a205a 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -1,22 +1,26 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Pp
 open CErrors
 open Util
 open Names
-open Term
+open Constr
+open EConstr
 open Termops
 open Declarations
 open Tacmach
 open Clenv
-open Sigma.Notations
-open Context.Named.Declaration
+open Tactypes
+
+module NamedDecl = Context.Named.Declaration
 
 (************************************************************************)
 (* Tacticals re-exported from the Refiner module                        *)
@@ -48,10 +52,8 @@ let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE
 let tclFAIL          = Refiner.tclFAIL
 let tclFAIL_lazy     = Refiner.tclFAIL_lazy
 let tclDO            = Refiner.tclDO
-let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS
 let tclPROGRESS      = Refiner.tclPROGRESS
 let tclSHOWHYPS      = Refiner.tclSHOWHYPS
-let tclNOTSAMEGOAL   = Refiner.tclNOTSAMEGOAL
 let tclTHENTRY       = Refiner.tclTHENTRY
 let tclIFTHENELSE    = Refiner.tclIFTHENELSE
 let tclIFTHENSELSE   = Refiner.tclIFTHENSELSE
@@ -68,9 +70,9 @@ let tclTHENSEQ       = tclTHENLIST
 
 let nthDecl m gl =
   try List.nth (pf_hyps gl) (m-1)
-  with Failure _ -> error "No such assumption."
+  with Failure _ -> user_err Pp.(str "No such assumption.")
 
-let nthHypId m gl = nthDecl m gl |> get_id
+let nthHypId m gl = nthDecl m gl |> NamedDecl.get_id
 let nthHyp m gl   = mkVar (nthHypId m gl)
 
 let lastDecl gl   = nthDecl 1 gl
@@ -79,9 +81,9 @@ let lastHyp gl    = nthHyp 1 gl
 
 let nLastDecls n gl =
   try List.firstn n (pf_hyps gl)
-  with Failure _ -> error "Not enough hypotheses in the goal."
+  with Failure _ -> user_err Pp.(str "Not enough hypotheses in the goal.")
 
-let nLastHypsId n gl = List.map get_id (nLastDecls n gl)
+let nLastHypsId n gl = List.map (NamedDecl.get_id) (nLastDecls n gl)
 let nLastHyps n gl   = List.map mkVar (nLastHypsId n gl)
 
 let onNthDecl m tac gl  = tac (nthDecl m gl) gl
@@ -99,7 +101,7 @@ let onNLastHypsId n tac = onHyps (nLastHypsId n) tac
 let onNLastHyps n tac   = onHyps (nLastHyps n) tac
 
 let afterHyp id gl =
-  fst (List.split_when (Id.equal id % get_id) (pf_hyps gl))
+  fst (List.split_when (NamedDecl.get_id %> Id.equal id) (pf_hyps gl))
 
 (***************************************)
 (*           Clause Tacticals          *)
@@ -151,11 +153,11 @@ type branch_args = {
   nassums    : int;         (* number of assumptions/letin to be introduced *)
   branchsign : bool list;   (* the signature of the branch.
                                true=assumption, false=let-in *)
-  branchnames : Tacexpr.intro_patterns}
+  branchnames : intro_patterns}
 
 type branch_assumptions = {
   ba        : branch_args;       (* the branch args *)
-  assums    : Context.Named.t}   (* the list of assumptions introduced *)
+  assums    : named_context}   (* the list of assumptions introduced *)
 
 open Misctypes
 
@@ -168,23 +170,23 @@ let fix_empty_or_and_pattern nv l =
   | IntroOrPattern [[]] -> IntroOrPattern (List.make nv [])
   | _ -> l
 
-let check_or_and_pattern_size check_and loc names branchsigns =
+let check_or_and_pattern_size ?loc check_and names branchsigns =
   let n = Array.length branchsigns in
   let msg p1 p2 = strbrk "a conjunctive pattern made of " ++ int p1 ++ (if p1 == p2 then mt () else str " or " ++ int p2) ++ str " patterns" in
   let err1 p1 p2 =
-    user_err_loc (loc,"",str "Expects " ++ msg p1 p2 ++ str ".") in
+    user_err ?loc  (str "Expects " ++ msg p1 p2 ++ str ".") in
   let errn n =
-    user_err_loc (loc,"",str "Expects a disjunctive pattern with " ++ int n
+    user_err ?loc  (str "Expects a disjunctive pattern with " ++ int n
 	++ str " branches.") in
   let err1' p1 p2 =
-    user_err_loc (loc,"",strbrk "Expects a disjunctive pattern with 1 branch or " ++ msg p1 p2 ++ str ".") in
-  let errforthcoming loc =
-    user_err_loc (loc,"",strbrk "Unexpected non atomic pattern.") in
+    user_err ?loc  (strbrk "Expects a disjunctive pattern with 1 branch or " ++ msg p1 p2 ++ str ".") in
+  let errforthcoming ?loc =
+    user_err ?loc  (strbrk "Unexpected non atomic pattern.") in
   match names with
   | IntroAndPattern l ->
       if not (Int.equal n 1) then errn n;
-      let l' = List.filter (function _,IntroForthcoming _ -> true | _,IntroNaming _ | _,IntroAction _ -> false) l in
-      if l' != [] then errforthcoming (fst (List.hd l'));
+      let l' = List.filter CAst.(function {v=IntroForthcoming _} -> true | {v=IntroNaming _} | {v=IntroAction _} -> false) l in
+      if l' != [] then errforthcoming ?loc:(List.hd l').CAst.loc;
       if check_and then
         let p1 = List.count (fun x -> x) branchsigns.(0) in
         let p2 = List.length branchsigns.(0) in
@@ -192,7 +194,7 @@ let check_or_and_pattern_size check_and loc 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) (Loc.ghost,IntroNaming IntroAnonymous) l)
+            (List.extend branchsigns.(0) (CAst.make @@ IntroNaming IntroAnonymous) l)
         else
           names
       else
@@ -205,27 +207,27 @@ let check_or_and_pattern_size check_and loc names branchsigns =
           err1' p1 p2 else errn n;
       names
 
-let get_and_check_or_and_pattern_gen check_and loc names branchsigns =
-  let names = check_or_and_pattern_size check_and loc names branchsigns in
+let get_and_check_or_and_pattern_gen ?loc check_and names branchsigns =
+  let names = check_or_and_pattern_size ?loc check_and names branchsigns in
   match names with
   | IntroAndPattern l -> [|l|]
   | IntroOrPattern l -> Array.of_list l
 
-let get_and_check_or_and_pattern = get_and_check_or_and_pattern_gen true
+let get_and_check_or_and_pattern ?loc = get_and_check_or_and_pattern_gen ?loc true
 
 let compute_induction_names_gen check_and branchletsigns = function
   | None ->
       Array.make (Array.length branchletsigns) []
-  | Some (loc,names) ->
+  | Some {CAst.loc;v=names} ->
       let names = fix_empty_or_and_pattern (Array.length branchletsigns) names in
-      get_and_check_or_and_pattern_gen check_and loc names branchletsigns
+      get_and_check_or_and_pattern_gen check_and ?loc names branchletsigns
 
 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 rec analrec c recargs =
-    match kind_of_term c, recargs with
+    match Constr.kind c, recargs with
     | Prod (_,_,c), recarg::rest ->
         let rest = analrec c rest in
         begin match Declareops.dest_recarg recarg with
@@ -236,12 +238,12 @@ let compute_constructor_signatures isrec ((_,k as ity),u) =
         end
     | LetIn (_,_,_,c), rest -> false :: analrec c rest
     | _, [] -> []
-    | _ -> anomaly (Pp.str "compute_constructor_signatures")
+    | _ -> anomaly (Pp.str "compute_constructor_signatures.")
   in
   let (mib,mip) = Global.lookup_inductive ity in
   let n = mib.mind_nparams in
   let lc =
-    Array.map (fun c -> snd (decompose_prod_n_assum n c)) mip.mind_nf_lc in
+    Array.map (fun c -> snd (Term.decompose_prod_n_assum n c)) mip.mind_nf_lc in
   let lrecargs = Declareops.dest_subterms mip.mind_recargs in
   Array.map2 analrec lc lrecargs
 
@@ -261,40 +263,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 -> pf_apply Evd.fresh_global gls gr) k
-
-(* computing the case/elim combinators *)
-
-let gl_make_elim ind gl =
-  let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in
-    pf_apply Evd.fresh_global gl gr
-
-let gl_make_case_dep ind gl =
-  let sigma = Sigma.Unsafe.of_evar_map (Tacmach.project gl) in
-  let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind true
-    (elimination_sort_of_goal gl)
-  in
-  (Sigma.to_evar_map sigma, r)
-
-let gl_make_case_nodep ind gl =
-  let sigma = Sigma.Unsafe.of_evar_map (Tacmach.project gl) in
-  let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind false
-    (elimination_sort_of_goal gl)
-  in
-  (Sigma.to_evar_map sigma, r)
-
-let make_elim_branch_assumptions ba gl =
-  let assums =
-    try List.rev (List.firstn ba.nassums (pf_hyps gl))
-    with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions") in
-  { ba = ba; assums = assums }
-
-let elim_on_ba tac ba gl = tac (make_elim_branch_assumptions ba gl) gl
-
-let make_case_branch_assumptions = make_elim_branch_assumptions
-
-let case_on_ba tac ba gl = tac (make_case_branch_assumptions ba gl) gl
-
+  pf_with_evars (fun gls -> on_snd EConstr.of_constr (pf_apply Evd.fresh_global gls gr)) k
 
 (** Tacticals of Ltac defined directly in term of Proofview *)
 module New = struct
@@ -311,7 +280,7 @@ module New = struct
     tclZERO (Refiner.FailError (lvl,lazy msg))
 
   let tclZEROMSG ?loc msg =
-    let err = UserError ("", msg) in
+    let err = UserError (None, msg) in
     let info = match loc with
     | None -> Exninfo.null
     | Some loc -> Loc.add_loc Exninfo.null loc
@@ -366,6 +335,16 @@ module New = struct
           catch_failerror e <*> t2
         end
     end
+
+  let tclORELSE0L t1 t2 =
+    tclINDEPENDENTL begin
+      tclORELSE
+        t1
+        begin fun e ->
+          catch_failerror e <*> t2
+        end
+    end
+
   let tclORELSE t1 t2 =
     tclORELSE0 (tclPROGRESS t1) t2
 
@@ -417,6 +396,9 @@ module New = struct
 
   let tclTRY t =
     tclORELSE0 t (tclUNIT ())
+  
+  let tclTRYb t =
+    tclORELSE0L (t <*> tclUNIT true) (tclUNIT false)
 
   let tclIFTHENELSE t1 t2 t3 =
     tclINDEPENDENT begin
@@ -428,8 +410,14 @@ module New = struct
     Proofview.tclIFCATCH t1
       (fun () -> tclDISPATCH (Array.to_list a))
       (fun _ -> t3)
+  let tclIFTHENFIRSTELSE t1 t2 t3 =
+    Proofview.tclIFCATCH t1
+      (fun () -> tclEXTEND [t2] (tclUNIT ()) [])
+      (fun _ -> t3)
   let tclIFTHENTRYELSEMUST t1 t2 =
     tclIFTHENELSE t1 (tclTRY t2) t2
+  let tclIFTHENFIRSTTRYELSEMUST t1 t2 =
+    tclIFTHENFIRSTELSE t1 (tclTRY t2) t2
 
   (* Try the first tactic that does not fail in a list of tactics *)
   let rec tclFIRST = function
@@ -478,19 +466,20 @@ module New = struct
 
   (* Select a subset of the goals *)
   let tclSELECT = function
-    | Tacexpr.SelectNth i -> Proofview.tclFOCUS i i
-    | Tacexpr.SelectList l -> Proofview.tclFOCUSLIST l
-    | Tacexpr.SelectId id -> Proofview.tclFOCUSID id
-    | Tacexpr.SelectAll -> fun tac -> tac
+    | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i
+    | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l
+    | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id
+    | Vernacexpr.SelectAll -> fun tac -> tac
 
   (* Check that holes in arguments have been resolved *)
 
   let check_evars env sigma extsigma origsigma =
     let rec is_undefined_up_to_restriction sigma evk =
+      if Evd.mem origsigma evk then None else
       let evi = Evd.find sigma evk in
       match Evd.evar_body evi with
       | Evd.Evar_empty -> Some (evk,evi)
-      | Evd.Evar_defined c -> match Term.kind_of_term c with
+      | Evd.Evar_defined c -> match Constr.kind c with
         | Term.Evar (evk,l) -> is_undefined_up_to_restriction sigma evk
         | _ -> 
           (* We make the assumption that there is no way to refine an
@@ -500,7 +489,7 @@ module New = struct
     let rest =
       Evd.fold_undefined (fun evk evi acc ->
         match is_undefined_up_to_restriction sigma evk with
-        | Some (evk',evi) when not (Evd.mem origsigma evk) -> (evk',evi)::acc
+        | Some (evk',evi) -> (evk',evi)::acc
         | _ -> acc)
         extsigma []
     in
@@ -508,7 +497,7 @@ module New = struct
     | [] -> ()
     | (evk,evi) :: _ ->
       let (loc,_) = evi.Evd.evar_source in
-      Pretype_errors.error_unsolvable_implicit loc env sigma evk None
+      Pretype_errors.error_unsolvable_implicit ?loc env sigma evk None
 
   let tclWITHHOLES accept_unresolved_holes tac sigma =
     tclEVARMAP >>= fun sigma_initial ->
@@ -529,12 +518,12 @@ module New = struct
         Proofview.Unsafe.tclEVARS sigma <*> tac >>= check_evars_if
 
   let tclDELAYEDWITHHOLES check x tac =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
       let env = Proofview.Goal.env gl in
       let sigma = Proofview.Goal.sigma gl in
-      let Sigma (x, sigma, _) = x.Tacexpr.delayed env sigma in
-      tclWITHHOLES check (tac x) (Sigma.to_evar_map sigma)
-    end }
+      let (sigma, x) = x env sigma in
+      tclWITHHOLES check (tac x) sigma
+    end
 
   let tclTIMEOUT n t =
     Proofview.tclOR
@@ -551,99 +540,99 @@ module New = struct
     let hyps = Proofview.Goal.hyps gl in
     try
       List.nth hyps (m-1)
-    with Failure _ -> CErrors.error "No such assumption."
+    with Failure _ -> CErrors.user_err Pp.(str "No such assumption.")
 
   let nLastDecls gl n =
     try List.firstn n (Proofview.Goal.hyps gl)
-    with Failure _ -> error "Not enough hypotheses in the goal."
+    with Failure _ -> CErrors.user_err Pp.(str "Not enough hypotheses in the goal.")
 
   let nthHypId m gl =
     (** We only use [id] *)
-    let gl = Proofview.Goal.assume gl in
-    nthDecl m gl |> get_id
+    nthDecl m gl |> NamedDecl.get_id
   let nthHyp m gl = 
     mkVar (nthHypId m gl)
 
   let onNthHypId m tac =
-    Proofview.Goal.enter { enter = begin fun gl -> tac (nthHypId m gl) end }
+    Proofview.Goal.enter begin fun gl -> tac (nthHypId m gl) end 
   let onNthHyp m tac =
-    Proofview.Goal.enter { enter = begin fun gl -> tac (nthHyp m gl) end }
+    Proofview.Goal.enter begin fun gl -> tac (nthHyp m gl) end
 
   let onLastHypId = onNthHypId 1
   let onLastHyp   = onNthHyp 1
 
   let onNthDecl m tac =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
       Proofview.tclUNIT (nthDecl m gl) >>= tac
-    end }
+    end
   let onLastDecl  = onNthDecl 1
 
   let ifOnHyp pred tac1 tac2 id =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
     let typ = Tacmach.New.pf_get_hyp_typ id gl in
     if pred (id,typ) then
       tac1 id
     else
       tac2 id
-    end }
+    end
 
-  let onHyps find tac = Proofview.Goal.nf_enter { enter = begin fun gl -> tac (find.enter gl) end }
+  let onHyps find tac = Proofview.Goal.enter begin fun gl -> tac (find gl) end
 
   let afterHyp id tac =
-    Proofview.Goal.enter { enter = begin fun gl ->
-    let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
-    let rem, _ = List.split_when (Id.equal id % get_id) hyps in
+    Proofview.Goal.enter begin fun gl ->
+    let hyps = Proofview.Goal.hyps gl in
+    let rem, _ = List.split_when (NamedDecl.get_id %> Id.equal id) hyps in
     tac rem
-    end }
+    end
 
   let fullGoal gl =
     let hyps = Tacmach.New.pf_ids_of_hyps gl in
     None :: List.map Option.make hyps
 
   let tryAllHyps tac =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
     let hyps = Tacmach.New.pf_ids_of_hyps gl in
     tclFIRST_PROGRESS_ON tac hyps
-    end }
+    end
   let tryAllHypsAndConcl tac =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
       tclFIRST_PROGRESS_ON tac (fullGoal gl)
-    end }
+    end
 
   let onClause tac cl =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
     let hyps = Tacmach.New.pf_ids_of_hyps gl in
     tclMAP tac (Locusops.simple_clause_of (fun () -> hyps) cl)
-    end }
+    end
 
   (* 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) =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in
+    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
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
-    (Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in
+    (Proofview.Goal.enter begin fun gl ->
+    let indclause = mk_clenv_from gl (c, t) in
     (* applying elimination_scheme just a little modified *)
-    let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl elim)) gl in
+    let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_unsafe_type_of gl elim)  in
     let indmv =
-      match kind_of_term (last_arg elimclause.templval.Evd.rebus) with
+      match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with
       | Meta mv -> mv
-      | _         -> anomaly (str"elimination")
+      | _         -> anomaly (str"elimination.")
     in
     let pmv =
-      let p, _ = decompose_app elimclause.templtyp.Evd.rebus in
-      match kind_of_term p with
+      let p, _ = decompose_app elimclause.evd elimclause.templtyp.Evd.rebus in
+      match EConstr.kind elimclause.evd p with
       | Meta p -> p
       | _ ->
 	  let name_elim =
-	    match kind_of_term elim with
-	    | Const (kn, _) -> string_of_con kn
-	    | Var id -> string_of_id id
+	    match EConstr.kind sigma elim with
+	    | Const (kn, _) -> Constant.to_string kn
+	    | Var id -> Id.to_string id
 	    | _ -> "\b"
 	  in
-	  errorlabstrm "Tacticals.general_elim_then_using"
+	  user_err ~hdr:"Tacticals.general_elim_then_using"
             (str "The elimination combinator " ++ str name_elim ++ str " is unknown.")
     in
     let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in
@@ -655,9 +644,9 @@ module New = struct
       | None   -> elimclause'
       | Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause'
     in
-    let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags elimclause') gl in
+    let clenv' = clenv_unique_resolver ~flags elimclause' gl in
     let after_tac i =
-      let (hd,largs) = decompose_app clenv'.templtyp.Evd.rebus in
+      let (hd,largs) = decompose_app clenv'.evd clenv'.templtyp.Evd.rebus in
       let ba = { branchsign = branchsigns.(i);
                  branchnames = brnames.(i);
                  nassums = List.length branchsigns.(i);
@@ -672,10 +661,68 @@ module New = struct
     Proofview.tclTHEN
       (Clenvtac.clenv_refine false clenv')
       (Proofview.tclEXTEND [] tclIDTAC branchtacs)
-    end }) end }
+    end) end
+
+  let elimination_sort_of_goal gl =
+    (** Retyping will expand evars anyway. *)
+    let c = Proofview.Goal.concl gl in
+    pf_apply Retyping.get_sort_family_of gl c
+
+  let elimination_sort_of_hyp id gl =
+    (** Retyping will expand evars anyway. *)
+    let c = pf_get_hyp_typ id gl in
+    pf_apply Retyping.get_sort_family_of gl c
+
+  let elimination_sort_of_clause id gl = match id with
+  | None -> elimination_sort_of_goal gl
+  | Some id -> elimination_sort_of_hyp id gl
+
+  (* computing the case/elim combinators *)
+
+  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)
+  end
+
+  let gl_make_case_dep (ind, u) = begin fun gl ->
+    let sigma = project gl in
+    let u = EInstance.kind (project gl) u in
+    let (sigma, r) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) true
+      (elimination_sort_of_goal gl)
+    in
+    (sigma, EConstr.of_constr r)
+  end
+
+  let gl_make_case_nodep (ind, u) = begin fun gl ->
+    let sigma = project gl in
+    let u = EInstance.kind sigma u in
+    let (sigma, r) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) false
+      (elimination_sort_of_goal gl)
+    in
+    (sigma, EConstr.of_constr r)
+  end
+
+  let make_elim_branch_assumptions ba hyps =
+    let assums =
+      try List.rev (List.firstn ba.nassums hyps)
+      with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions.") in
+    { ba = ba; assums = assums }
+
+  let elim_on_ba tac ba =
+    Proofview.Goal.enter begin fun gl ->
+    let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in
+    tac branches
+    end
+
+  let case_on_ba tac ba = 
+    Proofview.Goal.enter begin fun gl ->
+    let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in
+    tac branches
+    end
 
   let elimination_then tac c =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
     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
@@ -683,7 +730,7 @@ module New = struct
       | Some _ -> false,gl_make_case_dep
     in
     general_elim_then_using mkelim isrec None tac None ind (c, t)
-    end }
+    end
 
   let case_then_using =
     general_elim_then_using gl_make_case_dep false
@@ -691,38 +738,11 @@ module New = struct
   let case_nodep_then_using =
     general_elim_then_using gl_make_case_nodep false
 
-  let elim_on_ba tac ba =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let branches = Tacmach.New.of_old (make_elim_branch_assumptions ba) gl in
-    tac branches
-    end }
-
-  let case_on_ba tac ba = 
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let branches = Tacmach.New.of_old (make_case_branch_assumptions ba) gl in
-    tac branches
-    end }
-
-  let elimination_sort_of_goal gl =
-    (** Retyping will expand evars anyway. *)
-    let c = Proofview.Goal.concl (Goal.assume gl) in
-    pf_apply Retyping.get_sort_family_of gl c
-
-  let elimination_sort_of_hyp id gl =
-    (** Retyping will expand evars anyway. *)
-    let c = pf_get_hyp_typ id (Goal.assume gl) in
-    pf_apply Retyping.get_sort_family_of gl c
-
-  let elimination_sort_of_clause id gl = match id with
-  | None -> elimination_sort_of_goal gl
-  | Some id -> elimination_sort_of_hyp id gl
-
-  let pf_constr_of_global ref tac =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
-      let env = Proofview.Goal.env gl in
-      let sigma = Tacmach.New.project gl in
-      let (sigma, c) = Evd.fresh_global env sigma ref in
-      Proofview.Unsafe.tclEVARS sigma <*> (tac c)
-    end }
+  let pf_constr_of_global ref =
+    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