Imported Upstream version 8.5~beta1+dfsg

1 files changed, 236 insertions, 243 deletions

diff --git a/tactics/inv.ml b/tactics/inv.ml
index 73edaf86..5502356f 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -1,63 +1,40 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
 open Term
+open Vars
+open Context
 open Termops
 open Namegen
-open Global
-open Sign
 open Environ
 open Inductiveops
 open Printer
-open Reductionops
 open Retyping
-open Tacmach
-open Proof_type
-open Evar_refiner
-open Clenv
-open Tactics
-open Tacticals
+open Tacmach.New
+open Tacticals.New
 open Tactics
 open Elim
 open Equality
-open Typing
-open Pattern
-open Matching
-open Glob_term
-open Genarg
+open Misctypes
 open Tacexpr
+open Proofview.Notations
 
-let collect_meta_variables c =
-  let rec collrec acc c = match kind_of_term c with
-    | Meta mv -> mv::acc
-    | _ -> fold_constr collrec acc c
-  in
-  collrec [] c
-
-let check_no_metas clenv ccl =
-  if occur_meta ccl then
-    let metas = List.filter (fun m -> not (Evd.meta_defined clenv.evd m))
-      (collect_meta_variables ccl) in
-    let metas = List.map (Evd.meta_name clenv.evd) metas in
-    errorlabstrm "inversion"
-      (str ("Cannot find an instantiation for variable"^
-	       (if List.length metas = 1 then " " else "s ")) ++
-	 prlist_with_sep pr_comma pr_name metas
-	 (* ajouter "in " ++ pr_lconstr ccl mais il faut le bon contexte *))
+let clear hyps = Proofview.V82.tactic (clear hyps)
 
 let var_occurs_in_pf gl id =
-  let env = pf_env gl in
-  occur_var env id (pf_concl gl) or
-  List.exists (occur_var_in_decl env id) (pf_hyps gl)
+  let env = Proofview.Goal.env gl in
+  occur_var env id (Proofview.Goal.concl gl) ||
+  List.exists (occur_var_in_decl env id) (Proofview.Goal.hyps gl)
 
 (* [make_inv_predicate (ity,args) C]
 
@@ -88,16 +65,16 @@ let var_occurs_in_pf gl id =
 type inversion_status = Dep of constr option | NoDep
 
 let compute_eqn env sigma n i ai =
-  (ai, (mkRel (n-i),get_type_of env sigma (mkRel (n-i))))
+  (mkRel (n-i),get_type_of env sigma (mkRel (n-i)))
 
-let make_inv_predicate env sigma indf realargs id status concl =
+let make_inv_predicate env evd indf realargs id status concl =
   let nrealargs = List.length realargs in
   let (hyps,concl) =
     match status with
       | NoDep ->
 	  (* We push the arity and leave concl unchanged *)
 	  let hyps_arity,_ = get_arity env indf in
-	  (hyps_arity,concl)
+	    (hyps_arity,concl)
       | Dep dflt_concl ->
 	  if not (occur_var env id concl) then
 	    errorlabstrm "make_inv_predicate"
@@ -109,41 +86,53 @@ let make_inv_predicate env sigma indf realargs id status concl =
             match dflt_concl with
               | Some concl -> concl (*assumed it's some [x1..xn,H:I(x1..xn)]C*)
               | None ->
-		let sort = get_sort_family_of env sigma concl in
-		let p = make_arity env true indf (new_sort_in_family sort) in
-		Unification.abstract_list_all env (Evd.create_evar_defs sigma)
-		  p concl (realargs@[mkVar id]) in
+		let sort = get_sort_family_of env !evd concl in
+		let sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd sort in
+		let p = make_arity env true indf sort in
+		let evd',(p,ptyp) = Unification.abstract_list_all env
+                  !evd p concl (realargs@[mkVar id])
+		in evd := evd'; p in
 	  let hyps,bodypred = decompose_lam_n_assum (nrealargs+1) pred in
 	  (* We lift to make room for the equations *)
 	  (hyps,lift nrealargs bodypred)
   in
   let nhyps = rel_context_length hyps in
   let env' = push_rel_context hyps env in
-  let realargs' = List.map (lift nhyps) realargs in
-  let pairs = list_map_i (compute_eqn env' sigma nhyps) 0 realargs' in
   (* Now the arity is pushed, and we need to construct the pairs
    * ai,mkRel(n-i+1) *)
   (* Now, we can recurse down this list, for each ai,(mkRel k) whether to
      push <Ai>(mkRel k)=ai (when   Ai is closed).
    In any case, we carry along the rest of pairs *)
-  let rec build_concl eqns n = function
-    | [] -> (it_mkProd concl eqns,n)
-    | (ai,(xi,ti))::restlist ->
+  let eqdata = Coqlib.build_coq_eq_data () in
+  let rec build_concl eqns args n = function
+    | [] -> it_mkProd concl eqns, Array.rev_of_list args
+    | ai :: restlist ->
+        let ai = lift nhyps ai in
+        let (xi, ti) = compute_eqn env' !evd nhyps n ai in
         let (lhs,eqnty,rhs) =
           if closed0 ti then
 	    (xi,ti,ai)
           else
-	    make_iterated_tuple env' sigma ai (xi,ti)
+	    let sigma, res = make_iterated_tuple env' !evd ai (xi,ti) in
+	      evd := sigma; res
 	in
-        let eq_term = Coqlib.build_coq_eq () in
-        let eqn = applist (eq_term ,[eqnty;lhs;rhs]) in
-	build_concl ((Anonymous,lift n eqn)::eqns) (n+1) restlist
+        let eq_term = eqdata.Coqlib.eq in
+	let eq = Evarutil.evd_comb1 (Evd.fresh_global env) evd eq_term in
+        let eqn = applist (eq,[eqnty;lhs;rhs]) in
+        let eqns = (Anonymous, lift n eqn) :: eqns in
+        let refl_term = eqdata.Coqlib.refl in
+	let refl_term = Evarutil.evd_comb1 (Evd.fresh_global env) evd refl_term in
+        let refl = mkApp (refl_term, [|eqnty; rhs|]) in
+	let _ = Evarutil.evd_comb1 (Typing.e_type_of env) evd refl in
+        let args = refl :: args in
+        build_concl eqns args (succ n) restlist
   in
-  let (newconcl,neqns) = build_concl [] 0 pairs in
+  let (newconcl, args) = build_concl [] [] 0 realargs in
   let predicate = it_mkLambda_or_LetIn_name env newconcl hyps in
+  let _ = Evarutil.evd_comb1 (Typing.e_type_of env) evd predicate in
   (* OK - this predicate should now be usable by res_elimination_then to
      do elimination on the conclusion. *)
-  (predicate,neqns)
+  predicate, args
 
 (* The result of the elimination is a bunch of goals like:
 
@@ -189,13 +178,13 @@ let make_inv_predicate env sigma indf realargs id status concl =
    and introduces generalized hypotheis.
    Precondition: t=(mkVar id) *)
 
-let rec dependent_hyps id idlist gl =
+let dependent_hyps env id idlist gl =
   let rec dep_rec =function
     | [] -> []
     | (id1,_,_)::l ->
 	(* Update the type of id1: it may have been subject to rewriting *)
-	let d = pf_get_hyp gl id1 in
-	if occur_var_in_decl (Global.env()) id d
+	let d = pf_get_hyp id1 gl in
+	if occur_var_in_decl env id d
         then d :: dep_rec l
         else dep_rec l
   in
@@ -207,8 +196,6 @@ let split_dep_and_nodep hyps gl =
        if var_occurs_in_pf gl id then (d::l1,l2) else (l1,d::l2))
     hyps ([],[])
 
-open Coqlib
-
 (* Computation of dids is late; must have been done in rewrite_equations*)
 (* Will keep generalizing and introducing back and forth... *)
 (* Moreover, others hyps depending of dids should have been *)
@@ -280,21 +267,62 @@ Summary: nine useless hypotheses!
 Nota: with Inversion_clear, only four useless hypotheses
 *)
 
-let generalizeRewriteIntros tac depids id gls =
-  let dids = dependent_hyps id depids gls in
-  (tclTHENSEQ
+let generalizeRewriteIntros as_mode tac depids id =
+  Proofview.tclENV >>= fun env ->
+  Proofview.Goal.nf_enter begin fun gl ->
+  let dids = dependent_hyps env id depids gl in
+  let reintros = if as_mode then intros_replacing else intros_possibly_replacing in
+  (tclTHENLIST
     [bring_hyps dids; tac;
      (* may actually fail to replace if dependent in a previous eq *)
-     intros_replacing (ids_of_named_context dids)])
-  gls
-
-let rec tclMAP_i n tacfun = function
-  | [] -> tclDO n (tacfun None)
-  | a::l ->
-      if n=0 then error "Too many names."
-      else tclTHEN (tacfun (Some a)) (tclMAP_i (n-1) tacfun l)
+     reintros (ids_of_named_context dids)])
+  end
+
+let error_too_many_names pats =
+  let loc = Loc.join_loc (fst (List.hd pats)) (fst (List.last pats)) in
+  Proofview.tclENV >>= fun env ->
+  tclZEROMSG ~loc (
+    str "Unexpected " ++
+    str (String.plural (List.length pats) "introduction pattern") ++
+    str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr (snd (c env Evd.empty)))) pats ++
+    str ".")
+
+let rec get_names (allow_conj,issimple) (loc,pat as x) = match pat with
+  | IntroNaming IntroAnonymous | IntroForthcoming _ ->
+      error "Anonymous pattern not allowed for inversion equations."
+  | IntroNaming (IntroFresh _) ->
+      error "Fresh pattern not allowed for inversion equations."
+  | IntroAction IntroWildcard ->
+      error "Discarding pattern not allowed for inversion equations."
+  | IntroAction (IntroRewrite _) ->
+      error "Rewriting pattern not allowed for inversion equations."
+  | IntroAction (IntroOrAndPattern [[]]) when allow_conj -> (None, [])
+  | IntroAction (IntroOrAndPattern [(_,IntroNaming (IntroIdentifier id)) :: _ as l])
+      when allow_conj -> (Some id,l)
+  | IntroAction (IntroOrAndPattern [_]) ->
+      if issimple then
+        error"Conjunctive patterns not allowed for simple inversion equations."
+      else
+        error"Nested conjunctive patterns not allowed for inversion equations."
+  | IntroAction (IntroInjection l) ->
+      error "Injection patterns not allowed for inversion equations."
+  | IntroAction (IntroOrAndPattern l) ->
+      error "Disjunctive patterns not allowed for inversion equations."
+  | IntroAction (IntroApplyOn (c,pat)) ->
+      error "Apply patterns not allowed for inversion equations."
+  | IntroNaming (IntroIdentifier id) ->
+      (Some id,[x])
+
+let rec tclMAP_i allow_conj n tacfun = function
+  | [] -> tclDO n (tacfun (None,[]))
+  | a::l as l' ->
+      if Int.equal n 0 then error_too_many_names l'
+      else
+        tclTHEN
+          (tacfun (get_names allow_conj a))
+          (tclMAP_i allow_conj (n-1) tacfun l)
 
-let remember_first_eq id x = if !x = no_move then x := MoveAfter id
+let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id
 
 (* invariant: ProjectAndApply is responsible for erasing the clause
    which it is given as input
@@ -304,217 +332,177 @@ let remember_first_eq id x = if !x = no_move then x := MoveAfter id
    If it can discriminate then the goal is proved, if not tries to use it as
    a rewrite rule. It erases the clause which is given as input *)
 
-let projectAndApply thin id eqname names depids gls =
+let projectAndApply as_mode thin avoid id eqname names depids =
   let subst_hyp l2r id =
     tclTHEN (tclTRY(rewriteInConcl l2r (mkVar id)))
       (if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC))
   in
-  let substHypIfVariable tac id gls =
-    let (t,t1,t2) = Hipattern.dest_nf_eq gls (pf_get_hyp_typ gls id) in
+  let substHypIfVariable tac id =
+    Proofview.Goal.nf_enter begin fun gl ->
+    (** We only look at the type of hypothesis "id" *)
+    let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in
+    let (t,t1,t2) = Hipattern.dest_nf_eq gl hyp in
     match (kind_of_term t1, kind_of_term t2) with
-    | Var id1, _ -> generalizeRewriteIntros (subst_hyp true id) depids id1 gls
-    | _, Var id2 -> generalizeRewriteIntros (subst_hyp false id) depids id2 gls
-    | _ -> tac id gls
+    | Var id1, _ -> generalizeRewriteIntros as_mode (subst_hyp true id) depids id1
+    | _, Var id2 -> generalizeRewriteIntros as_mode (subst_hyp false id) depids id2
+    | _ -> tac id
+    end
   in
-  let deq_trailer id neqns =
-    tclTHENSEQ
-      [(if names <> [] then clear [id] else tclIDTAC);
-       (tclMAP_i neqns (fun idopt ->
+  let deq_trailer id clear_flag _ neqns =
+    assert (clear_flag == None);
+    tclTHENLIST
+      [if as_mode then clear [id] else tclIDTAC;
+       (tclMAP_i (false,false) neqns (function (idopt,_) ->
 	 tclTRY (tclTHEN
-	   (intro_move idopt no_move)
+	   (intro_move_avoid idopt avoid MoveLast)
 	   (* try again to substitute and if still not a variable after *)
 	   (* decomposition, arbitrarily try to rewrite RL !? *)
-	   (tclTRY (onLastHypId (substHypIfVariable (subst_hyp false))))))
+	   (tclTRY (onLastHypId (substHypIfVariable (fun id -> subst_hyp false id))))))
 	 names);
-       (if names = [] then clear [id] else tclIDTAC)]
+       (if as_mode then tclIDTAC else clear [id])]
+          (* Doing the above late breaks the computation of dids in 
+             generalizeRewriteIntros, and hence breaks proper intros_replacing
+             but it is needed for compatibility *)
   in
   substHypIfVariable
     (* If no immediate variable in the equation, try to decompose it *)
     (* and apply a trailer which again try to substitute *)
     (fun id ->
       dEqThen false (deq_trailer id)
-	(Some (ElimOnConstr (mkVar id,NoBindings))))
+	(Some (None,ElimOnConstr (mkVar id,NoBindings))))
     id
-    gls
-
-(* Inversion qui n'introduit pas les hypotheses, afin de pouvoir les nommer
-   soi-meme (proposition de Valerie). *)
-let rewrite_equations_gene othin neqns ba gl =
-  let (depids,nodepids) = split_dep_and_nodep ba.assums gl in
-  let rewrite_eqns =
-    match othin with
-      | Some thin ->
-          onLastHypId
-            (fun last ->
-              tclTHENSEQ
-                [tclDO neqns
-                     (tclTHEN intro
-                        (onLastHypId
-                           (fun id ->
-                              tclTRY
-			        (projectAndApply thin id (ref no_move)
-				  [] depids))));
-                 onHyps (compose List.rev (afterHyp last)) bring_hyps;
-                 onHyps (afterHyp last)
-                   (compose clear ids_of_named_context)])
-      | None -> tclIDTAC
-  in
-  (tclTHENSEQ
-    [tclDO neqns intro;
-     bring_hyps nodepids;
-     clear (ids_of_named_context nodepids);
-     onHyps (compose List.rev (nLastDecls neqns)) bring_hyps;
-     onHyps (nLastDecls neqns) (compose clear ids_of_named_context);
-     rewrite_eqns;
-     tclMAP (fun (id,_,_ as d) ->
-               (tclORELSE (clear [id])
-                 (tclTHEN (bring_hyps [d]) (clear [id]))))
-       depids])
-  gl
+
+let nLastDecls i tac =
+  Proofview.Goal.nf_enter (fun gl -> tac (nLastDecls gl i))
 
 (* Introduction of the equations on arguments
    othin: discriminates Simple Inversion, Inversion and Inversion_clear
      None: the equations are introduced, but not rewritten
      Some thin: the equations are rewritten, and cleared if thin is true *)
 
-let rec get_names allow_conj (loc,pat) = match pat with
-  | IntroWildcard ->
-      error "Discarding pattern not allowed for inversion equations."
-  | IntroAnonymous | IntroForthcoming _ ->
-      error "Anonymous pattern not allowed for inversion equations."
-  | IntroFresh _ ->
-      error "Fresh pattern not allowed for inversion equations."
-  | IntroRewrite _->
-      error "Rewriting pattern not allowed for inversion equations."
-  | IntroOrAndPattern [l] ->
-      if allow_conj then
-	if l = [] then (None,[]) else
-	  let l = List.map (fun id -> Option.get (fst (get_names false id))) l in
-	  (Some (List.hd l), l)
-      else
-	error"Nested conjunctive patterns not allowed for inversion equations."
-  | IntroOrAndPattern l ->
-      error "Disjunctive patterns not allowed for inversion equations."
-  | IntroIdentifier id ->
-      (Some id,[id])
-
-let extract_eqn_names = function
-  | None -> None,[]
-  | Some x -> x
-
-let rewrite_equations othin neqns names ba gl =
-  let names = List.map (get_names true) names in
-  let (depids,nodepids) = split_dep_and_nodep ba.assums gl in
-  let rewrite_eqns =
-    let first_eq = ref no_move in
-    match othin with
-      | Some thin ->
-          tclTHENSEQ
-            [onHyps (compose List.rev (nLastDecls neqns)) bring_hyps;
-             onHyps (nLastDecls neqns) (compose clear ids_of_named_context);
-	     tclMAP_i neqns (fun o ->
-	       let idopt,names = extract_eqn_names o in
+let rewrite_equations as_mode othin neqns names ba =
+  Proofview.Goal.nf_enter begin fun gl ->
+  let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in
+  let first_eq = ref MoveLast in
+  let avoid = if as_mode then List.map pi1 nodepids else [] in
+  match othin with
+    | Some thin ->
+        tclTHENLIST
+            [tclDO neqns intro;
+             bring_hyps nodepids;
+             clear (ids_of_named_context nodepids);
+             (nLastDecls neqns (fun ctx -> bring_hyps (List.rev ctx)));
+             (nLastDecls neqns (fun ctx -> clear (ids_of_named_context ctx)));
+	     tclMAP_i (true,false) neqns (fun (idopt,names) ->
                (tclTHEN
-		 (intro_move idopt no_move)
+		 (intro_move_avoid idopt avoid MoveLast)
 		 (onLastHypId (fun id ->
-		   tclTRY (projectAndApply thin id first_eq names depids)))))
+		   tclTRY (projectAndApply as_mode thin avoid id first_eq names depids)))))
 	       names;
-	     tclMAP (fun (id,_,_) gl ->
-	       intro_move None (if thin then no_move else !first_eq) gl)
+	     tclMAP (fun (id,_,_) -> tclIDTAC >>= fun () -> (* delay for [first_eq]. *)
+               let idopt = if as_mode then Some id else None in
+	       intro_move idopt (if thin then MoveLast else !first_eq))
 	       nodepids;
-	     tclMAP (fun (id,_,_) -> tclTRY (clear [id])) depids]
-      | None -> tclIDTAC
-  in
-  (tclTHENSEQ
-    [tclDO neqns intro;
-     bring_hyps nodepids;
-     clear (ids_of_named_context nodepids);
-     rewrite_eqns])
-  gl
+	     (tclMAP (fun (id,_,_) -> tclTRY (clear [id])) depids)]
+    | None ->
+        (* simple inversion *)
+        if as_mode then
+          tclMAP_i (false,true) neqns (fun (idopt,_) ->
+	    intro_move idopt MoveLast) names
+        else
+          (tclTHENLIST
+             [tclDO neqns intro;
+              bring_hyps nodepids;
+              clear (ids_of_named_context nodepids)])
+  end
 
 let interp_inversion_kind = function
   | SimpleInversion -> None
   | FullInversion -> Some false
   | FullInversionClear -> Some true
 
-let rewrite_equations_tac (gene, othin) id neqns names ba =
+let rewrite_equations_tac as_mode othin id neqns names ba =
   let othin = interp_inversion_kind othin in
-  let tac =
-    if gene then rewrite_equations_gene othin neqns ba
-    else rewrite_equations othin neqns names ba in
-  if othin = Some true (* if Inversion_clear, clear the hypothesis *) then
+  let tac = rewrite_equations as_mode othin neqns names ba in
+  match othin with
+  | Some true (* if Inversion_clear, clear the hypothesis *) ->
     tclTHEN tac (tclTRY (clear [id]))
-  else
+  | _ ->
     tac
 
-
-let raw_inversion inv_kind id status names gl =
-  let env = pf_env gl and sigma = project gl in
-  let c = mkVar id in
-  let (ind,t) =
-    try pf_reduce_to_atomic_ind gl (pf_type_of gl c)
-    with UserError _ ->
-      errorlabstrm "raw_inversion"
-	(str ("The type of "^(string_of_id id)^" is not inductive.")) in
-  let indclause = mk_clenv_from gl (c,t) in
-  let ccl = clenv_type indclause in
-  check_no_metas indclause ccl;
-  let IndType (indf,realargs) = find_rectype env sigma ccl in
-  let (elim_predicate,neqns) =
-    make_inv_predicate env sigma indf realargs id status (pf_concl gl) in
-  let (cut_concl,case_tac) =
-    if status <> NoDep & (dependent c (pf_concl gl)) then
-      Reduction.beta_appvect elim_predicate (Array.of_list (realargs@[c])),
-      case_then_using
-    else
-      Reduction.beta_appvect elim_predicate (Array.of_list realargs),
-      case_nodep_then_using
-  in
-  (tclTHENS
-     (assert_tac Anonymous cut_concl)
-     [case_tac names
-       (introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns))
-       (Some elim_predicate) ([],[]) ind indclause;
-      onLastHypId
-        (fun id ->
-           (tclTHEN
-              (apply_term (mkVar id)
-                 (list_tabulate (fun _ -> Evarutil.mk_new_meta()) neqns))
-              reflexivity))])
-  gl
+let raw_inversion inv_kind id status names =
+  Proofview.Goal.nf_enter begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
+    let env = Proofview.Goal.env gl in
+    let concl = Proofview.Goal.concl gl in
+    let c = mkVar id in
+    let (ind, t) =
+      try pf_apply Tacred.reduce_to_atomic_ind gl (pf_type_of gl c)
+      with UserError _ ->
+        let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in
+        Errors.errorlabstrm "" msg
+    in
+    let IndType (indf,realargs) = find_rectype env sigma t in
+    let evdref = ref sigma in
+    let (elim_predicate, args) =
+      make_inv_predicate env evdref indf realargs id status concl in
+    let sigma = !evdref in
+    let (cut_concl,case_tac) =
+      if status != NoDep && (dependent c concl) then
+        Reduction.beta_appvect elim_predicate (Array.of_list (realargs@[c])),
+        case_then_using
+      else
+        Reduction.beta_appvect elim_predicate (Array.of_list realargs),
+        case_nodep_then_using
+    in
+    let refined id =
+      let prf = mkApp (mkVar id, args) in
+      Proofview.Refine.refine (fun h -> h, prf)
+    in
+    let neqns = List.length realargs in
+    let as_mode = names != None in
+    tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+      (tclTHENS
+        (assert_before Anonymous cut_concl)
+        [case_tac names
+            (introCaseAssumsThen
+               (rewrite_equations_tac as_mode inv_kind id neqns))
+            (Some elim_predicate) ind (c, t);
+        onLastHypId (fun id -> tclTHEN (refined id) reflexivity)])
+  end
 
 (* Error messages of the inversion tactics *)
-let wrap_inv_error id = function
+let wrap_inv_error id = function (e, info) -> match e with
   | Indrec.RecursionSchemeError
       (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Prop Pos as k),i)) ->
-      errorlabstrm ""
+      Proofview.tclENV >>= fun env ->
+      tclZEROMSG (
 	(strbrk "Inversion would require case analysis on sort " ++
-	pr_sort k ++
+	pr_sort Evd.empty k ++
 	strbrk " which is not allowed for inductive definition " ++
-	pr_inductive (Global.env()) i ++ str ".")
-  | e -> raise e
+	pr_inductive env (fst i) ++ str "."))
+  | e -> Proofview.tclZERO ~info e
 
 (* The most general inversion tactic *)
-let inversion inv_kind status names id gls =
-  try (raw_inversion inv_kind id status names) gls
-  with e when Errors.noncritical e -> wrap_inv_error id e
+let inversion inv_kind status names id =
+  Proofview.tclORELSE
+    (raw_inversion inv_kind id status names)
+    (wrap_inv_error id)
 
 (* Specializing it... *)
 
-let inv_gen gene thin status names =
-  try_intros_until (inversion (gene,thin) status names)
+let inv_gen thin status names =
+  try_intros_until (inversion thin status names)
 
 open Tacexpr
 
-let inv k = inv_gen false k NoDep
+let inv k = inv_gen k NoDep
 
-let half_inv_tac id  = inv SimpleInversion None (NamedHyp id)
 let inv_tac id       = inv FullInversion None (NamedHyp id)
 let inv_clear_tac id = inv FullInversionClear None (NamedHyp id)
 
-let dinv k c = inv_gen false k (Dep c)
+let dinv k c = inv_gen k (Dep c)
 
-let half_dinv_tac id  = dinv SimpleInversion None None (NamedHyp id)
 let dinv_tac id       = dinv FullInversion None None (NamedHyp id)
 let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id)
 
@@ -522,25 +510,30 @@ let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id)
  * perform inversion on the named hypothesis.  After, it will intro them
  * back to their places in the hyp-list. *)
 
-let invIn k names ids id gls =
-  let hyps = List.map (pf_get_hyp gls) ids in
-  let nb_prod_init = nb_prod (pf_concl gls) in
-  let intros_replace_ids gls =
-    let nb_of_new_hyp =
-      nb_prod (pf_concl gls) - (List.length hyps + nb_prod_init)
+let invIn k names ids id =
+  Proofview.Goal.nf_enter begin fun gl ->
+    let hyps = List.map (fun id -> pf_get_hyp id gl) ids in
+    let concl = Proofview.Goal.concl gl in
+    let nb_prod_init = nb_prod concl in
+    let intros_replace_ids =
+      Proofview.Goal.enter begin fun gl ->
+        let concl = pf_nf_concl gl in
+        let nb_of_new_hyp =
+          nb_prod concl - (List.length hyps + nb_prod_init)
+        in
+        if nb_of_new_hyp < 1 then
+          intros_replacing ids
+        else
+          tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids)
+      end
     in
-    if nb_of_new_hyp < 1 then
-      intros_replacing ids gls
-    else
-      tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids) gls
-  in
-  try
-    (tclTHENSEQ
-      [bring_hyps hyps;
-       inversion (false,k) NoDep names id;
-       intros_replace_ids])
-    gls
-  with e when Errors.noncritical e -> wrap_inv_error id e
+    Proofview.tclORELSE
+      (tclTHENLIST
+         [bring_hyps hyps;
+          inversion k NoDep names id;
+          intros_replace_ids])
+      (wrap_inv_error id)
+  end
 
 let invIn_gen k names idl = try_intros_until (invIn k names idl)