1 files changed, 123 insertions, 91 deletions

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 1afc6500b..adf926958 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -18,6 +18,7 @@ open Util
 open Names
 open Nameops
 open Term
+open EConstr
 open Tacticals
 open Tacmach
 open Tactics
@@ -37,7 +38,7 @@ open OmegaSolver
 (* Added by JCF, 09/03/98 *)
 
 let elim_id id =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     simplest_elim (Tacmach.New.pf_global id gl)
   end }
 let resolve_id id gl = Proofview.V82.of_tactic (apply (pf_global gl id)) gl
@@ -172,8 +173,8 @@ let tag_hypothesis,tag_of_hyp, hyp_of_tag, clear_tags =
 let hide_constr,find_constr,clear_constr_tables,dump_tables =
   let l = ref ([]:(constr * (Id.t * Id.t * bool)) list) in
   (fun h id eg b -> l := (h,(id,eg,b)):: !l),
-  (fun h ->
-    try List.assoc_f eq_constr_nounivs h !l with Not_found -> failwith "find_contr"),
+  (fun sigma h ->
+    try List.assoc_f (eq_constr_nounivs sigma) h !l with Not_found -> failwith "find_contr"),
   (fun () -> l := []),
   (fun () -> !l)
 
@@ -197,6 +198,7 @@ let coq_modules =
   init_modules @arith_modules @ [logic_dir] @ zarith_base_modules
     @ [["Coq"; "omega"; "OmegaLemmas"]]
 
+let gen_constant_in_modules n m s = EConstr.of_constr (gen_constant_in_modules n m s)
 let init_constant = gen_constant_in_modules "Omega" init_modules
 let constant = gen_constant_in_modules "Omega" coq_modules
 
@@ -348,11 +350,18 @@ let coq_not_iff = lazy (constant "not_iff")
 let coq_not_not = lazy (constant "not_not")
 let coq_imp_simp = lazy (constant "imp_simp")
 let coq_iff = lazy (constant "iff")
+let coq_not = lazy (init_constant "not")
+let coq_and = lazy (init_constant "and")
+let coq_or = lazy (init_constant "or")
+let coq_eq = lazy (init_constant "eq")
+let coq_ex = lazy (init_constant "ex")
+let coq_False = lazy (init_constant "False")
+let coq_True = lazy (init_constant "True")
 
 (* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *)
 
 (* For unfold *)
-let evaluable_ref_of_constr s c = match kind_of_term (Lazy.force c) with
+let evaluable_ref_of_constr s c = match EConstr.kind Evd.empty (Lazy.force c) with
   | Const (kn,u) when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) ->
       EvalConstRef kn
   | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant"))
@@ -364,21 +373,21 @@ let sp_Zle = lazy (evaluable_ref_of_constr "Z.le" coq_Zle)
 let sp_Zgt = lazy (evaluable_ref_of_constr "Z.gt" coq_Zgt)
 let sp_Zge = lazy (evaluable_ref_of_constr "Z.ge" coq_Zge)
 let sp_Zlt = lazy (evaluable_ref_of_constr "Z.lt" coq_Zlt)
-let sp_not = lazy (evaluable_ref_of_constr "not" (lazy (build_coq_not ())))
+let sp_not = lazy (evaluable_ref_of_constr "not" coq_not)
 
 let mk_var v = mkVar (Id.of_string v)
 let mk_plus t1 t2 = mkApp (Lazy.force coq_Zplus, [| t1; t2 |])
 let mk_times t1 t2 = mkApp (Lazy.force coq_Zmult, [| t1; t2 |])
 let mk_minus t1 t2 = mkApp (Lazy.force coq_Zminus, [| t1;t2 |])
-let mk_eq t1 t2 = mkApp (Universes.constr_of_global (build_coq_eq ()),
+let mk_eq t1 t2 = mkApp (Lazy.force coq_eq,
 			 [| Lazy.force coq_Z; t1; t2 |])
 let mk_le t1 t2 = mkApp (Lazy.force coq_Zle, [| t1; t2 |])
 let mk_gt t1 t2 = mkApp (Lazy.force coq_Zgt, [| t1; t2 |])
 let mk_inv t = mkApp (Lazy.force coq_Zopp, [| t |])
-let mk_and t1 t2 =  mkApp (build_coq_and (), [| t1; t2 |])
-let mk_or t1 t2 =  mkApp (build_coq_or (), [| t1; t2 |])
-let mk_not t = mkApp (build_coq_not (), [| t |])
-let mk_eq_rel t1 t2 = mkApp (Universes.constr_of_global (build_coq_eq ()),
+let mk_and t1 t2 =  mkApp (Lazy.force coq_and, [| t1; t2 |])
+let mk_or t1 t2 =  mkApp (Lazy.force coq_or, [| t1; t2 |])
+let mk_not t = mkApp (Lazy.force coq_not, [| t |])
+let mk_eq_rel t1 t2 = mkApp (Lazy.force coq_eq,
 			     [| Lazy.force coq_comparison; t1; t2 |])
 let mk_inj t = mkApp (Lazy.force coq_Z_of_nat, [| t |])
 
@@ -420,22 +429,23 @@ type result =
    the term parts that we manipulate, but rather Var's.
    Said otherwise: all constr manipulated here are closed *)
 
-let destructurate_prop t =
-  let c, args = decompose_app t in
-  match kind_of_term c, args with
-    | _, [_;_;_] when is_global (build_coq_eq ()) c -> Kapp (Eq,args)
+let destructurate_prop sigma t =
+  let eq_constr c1 c2 = eq_constr sigma c1 c2 in
+  let c, args = decompose_app sigma t in
+  match EConstr.kind sigma c, args with
+    | _, [_;_;_] when eq_constr (Lazy.force coq_eq) c -> Kapp (Eq,args)
     | _, [_;_] when eq_constr c (Lazy.force coq_neq) -> Kapp (Neq,args)
     | _, [_;_] when eq_constr c (Lazy.force coq_Zne) -> Kapp (Zne,args)
     | _, [_;_] when eq_constr c (Lazy.force coq_Zle) -> Kapp (Zle,args)
     | _, [_;_] when eq_constr c (Lazy.force coq_Zlt) -> Kapp (Zlt,args)
     | _, [_;_] when eq_constr c (Lazy.force coq_Zge) -> Kapp (Zge,args)
     | _, [_;_] when eq_constr c (Lazy.force coq_Zgt) -> Kapp (Zgt,args)
-    | _, [_;_] when eq_constr c (build_coq_and ()) -> Kapp (And,args)
-    | _, [_;_] when eq_constr c (build_coq_or ()) -> Kapp (Or,args)
+    | _, [_;_] when eq_constr c (Lazy.force coq_and) -> Kapp (And,args)
+    | _, [_;_] when eq_constr c (Lazy.force coq_or) -> Kapp (Or,args)
     | _, [_;_] when eq_constr c (Lazy.force coq_iff) -> Kapp (Iff, args)
-    | _, [_] when eq_constr c (build_coq_not ()) -> Kapp (Not,args)
-    | _, [] when eq_constr c (build_coq_False ()) -> Kapp (False,args)
-    | _, [] when eq_constr c (build_coq_True ()) -> Kapp (True,args)
+    | _, [_] when eq_constr c (Lazy.force coq_not) -> Kapp (Not,args)
+    | _, [] when eq_constr c (Lazy.force coq_False) -> Kapp (False,args)
+    | _, [] when eq_constr c (Lazy.force coq_True) -> Kapp (True,args)
     | _, [_;_] when eq_constr c (Lazy.force coq_le) -> Kapp (Le,args)
     | _, [_;_] when eq_constr c (Lazy.force coq_lt) -> Kapp (Lt,args)
     | _, [_;_] when eq_constr c (Lazy.force coq_ge) -> Kapp (Ge,args)
@@ -451,16 +461,18 @@ let destructurate_prop t =
     | Prod (Name _,_,_),[] -> error "Omega: Not a quantifier-free goal"
     | _ -> Kufo
 
-let destructurate_type t =
-  let c, args = decompose_app t in
-  match kind_of_term c, args with
+let destructurate_type sigma t =
+  let eq_constr c1 c2 = eq_constr sigma c1 c2 in
+  let c, args = decompose_app sigma t in
+  match EConstr.kind sigma c, args with
     | _, [] when eq_constr c (Lazy.force coq_Z) -> Kapp (Z,args)
     | _, [] when eq_constr c (Lazy.force coq_nat) -> Kapp (Nat,args)
     | _ -> Kufo
 
-let destructurate_term t =
-  let c, args = decompose_app t in
-  match kind_of_term c, args with
+let destructurate_term sigma t =
+  let eq_constr c1 c2 = eq_constr sigma c1 c2 in
+  let c, args = decompose_app sigma t in
+  match EConstr.kind sigma c, args with
     | _, [_;_] when eq_constr c (Lazy.force coq_Zplus) -> Kapp (Zplus,args)
     | _, [_;_] when eq_constr c (Lazy.force coq_Zmult) -> Kapp (Zmult,args)
     | _, [_;_] when eq_constr c (Lazy.force coq_Zminus) -> Kapp (Zminus,args)
@@ -480,15 +492,16 @@ let destructurate_term t =
     | Var id,[] -> Kvar id
     | _ -> Kufo
 
-let recognize_number t =
+let recognize_number sigma t =
+  let eq_constr c1 c2 = eq_constr sigma c1 c2 in
   let rec loop t =
-    match decompose_app t with
+    match decompose_app sigma t with
       | f, [t] when eq_constr f (Lazy.force coq_xI) -> one + two * loop t
       | f, [t] when eq_constr f (Lazy.force coq_xO) -> two * loop t
       | f, [] when eq_constr f (Lazy.force coq_xH) -> one
       | _ -> failwith "not a number"
   in
-  match decompose_app t with
+  match decompose_app sigma t with
     | f, [t] when eq_constr f (Lazy.force coq_Zpos) -> loop t
     | f, [t] when eq_constr f (Lazy.force coq_Zneg) -> neg (loop t)
     | f, [] when eq_constr f (Lazy.force coq_Z0) -> zero
@@ -504,9 +517,9 @@ type constr_path =
   | P_ARITY
   | P_ARG
 
-let context operation path (t : constr) =
+let context sigma operation path (t : constr) =
   let rec loop i p0 t =
-    match (p0,kind_of_term t) with
+    match (p0,EConstr.kind sigma t) with
       | (p, Cast (c,k,t)) -> mkCast (loop i p c,k,t)
       | ([], _) -> operation i t
       | ((P_APP n :: p),  App (f,v)) ->
@@ -517,7 +530,7 @@ let context operation path (t : constr) =
 	  let v' = Array.copy v in
 	  v'.(n) <- loop i p v'.(n); (mkCase (ci,q,c,v'))
       | ((P_ARITY :: p),  App (f,l)) ->
-	  appvect (loop i p f,l)
+	  mkApp (loop i p f,l)
       | ((P_ARG :: p),  App (f,v)) ->
 	  let v' = Array.copy v in
 	  v'.(0) <- loop i p v'.(0); mkApp (f,v')
@@ -542,8 +555,8 @@ let context operation path (t : constr) =
   in
   loop 1 path t
 
-let occurrence path (t : constr) =
-  let rec loop p0 t = match (p0,kind_of_term t) with
+let occurrence sigma path (t : constr) =
+  let rec loop p0 t = match (p0,EConstr.kind sigma t) with
     | (p, Cast (c,_,_)) -> loop p c
     | ([], _) -> t
     | ((P_APP n :: p),  App (f,v)) -> loop p v.(pred n)
@@ -562,13 +575,13 @@ let occurrence path (t : constr) =
   in
   loop path t
 
-let abstract_path typ path t =
+let abstract_path sigma typ path t =
   let term_occur = ref (mkRel 0) in
-  let abstract = context (fun i t -> term_occur:= t; mkRel i) path t in
+  let abstract = context sigma (fun i t -> term_occur:= t; mkRel i) path t in
   mkLambda (Name (Id.of_string "x"), typ, abstract), !term_occur
 
 let focused_simpl path gl =
-  let newc = context (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
+  let newc = context (project gl) (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
   Proofview.V82.of_tactic (convert_concl_no_check newc DEFAULTcast) gl
 
 let focused_simpl path = focused_simpl path
@@ -631,7 +644,7 @@ let mkNewMeta () = mkMeta (Evarutil.new_meta())
 
 let clever_rewrite_base_poly typ p result theorem gl =
   let full = pf_concl gl in
-  let (abstracted,occ) = abstract_path typ (List.rev p) full in
+  let (abstracted,occ) = abstract_path (project gl) typ (List.rev p) full in
   let t =
     applist
       (mkLambda
@@ -662,8 +675,8 @@ let clever_rewrite_gen_nat p result (t,args) =
 
 let clever_rewrite p vpath t gl =
   let full = pf_concl gl in
-  let (abstracted,occ) = abstract_path (Lazy.force coq_Z) (List.rev p) full in
-  let vargs = List.map (fun p -> occurrence p occ) vpath in
+  let (abstracted,occ) = abstract_path (project gl) (Lazy.force coq_Z) (List.rev p) full in
+  let vargs = List.map (fun p -> occurrence (project gl) p occ) vpath in
   let t' = applist(t, (vargs @ [abstracted])) in
   exact (applist(t',[mkNewMeta()])) gl
 
@@ -907,10 +920,10 @@ let rec negate p = function
   | Oz i -> [focused_simpl p],Oz(neg i)
   | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zopp, [| c |]))
 
-let rec transform p t =
+let rec transform sigma p t =
   let default isnat t' =
     try
-      let v,th,_ = find_constr t' in
+      let v,th,_ = find_constr sigma t' in
       [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v
     with e when CErrors.noncritical e ->
       let v = new_identifier_var ()
@@ -918,29 +931,29 @@ let rec transform p t =
       hide_constr t' v th isnat;
       [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v
   in
-  try match destructurate_term t with
+  try match destructurate_term sigma t with
     | Kapp(Zplus,[t1;t2]) ->
-	let tac1,t1' = transform (P_APP 1 :: p) t1
-	and tac2,t2' = transform (P_APP 2 :: p) t2 in
+	let tac1,t1' = transform sigma (P_APP 1 :: p) t1
+	and tac2,t2' = transform sigma (P_APP 2 :: p) t2 in
 	let tac,t' = shuffle p (t1',t2') in
 	tac1 @ tac2 @ tac, t'
     | Kapp(Zminus,[t1;t2]) ->
 	let tac,t =
-	  transform p
+	  transform sigma p
 	    (mkApp (Lazy.force coq_Zplus,
 		     [| t1; (mkApp (Lazy.force coq_Zopp, [| t2 |])) |])) in
 	Proofview.V82.of_tactic (unfold sp_Zminus) :: tac,t
     | Kapp(Zsucc,[t1]) ->
-	let tac,t = transform p (mkApp (Lazy.force coq_Zplus,
+	let tac,t = transform sigma p (mkApp (Lazy.force coq_Zplus,
 					 [| t1; mk_integer one |])) in
 	Proofview.V82.of_tactic (unfold sp_Zsucc) :: tac,t
     | Kapp(Zpred,[t1]) ->
-	let tac,t = transform p (mkApp (Lazy.force coq_Zplus,
+	let tac,t = transform sigma p (mkApp (Lazy.force coq_Zplus,
 					 [| t1; mk_integer negone |])) in
 	Proofview.V82.of_tactic (unfold sp_Zpred) :: tac,t
    | Kapp(Zmult,[t1;t2]) ->
-       let tac1,t1' = transform (P_APP 1 :: p) t1
-       and tac2,t2' = transform (P_APP 2 :: p) t2 in
+       let tac1,t1' = transform sigma (P_APP 1 :: p) t1
+       and tac2,t2' = transform sigma (P_APP 2 :: p) t2 in
        begin match t1',t2' with
          | (_,Oz n) -> let tac,t' = scalar p n t1' in tac1 @ tac2 @ tac,t'
          | (Oz n,_) ->
@@ -951,11 +964,11 @@ let rec transform p t =
          | _ -> default false t
        end
    | Kapp((Zpos|Zneg|Z0),_) ->
-       (try ([],Oz(recognize_number t))
+       (try ([],Oz(recognize_number sigma t))
         with e when CErrors.noncritical e -> default false t)
    | Kvar s -> [],Oatom s
    | Kapp(Zopp,[t]) ->
-       let tac,t' = transform (P_APP 1 :: p) t in
+       let tac,t' = transform sigma (P_APP 1 :: p) t in
        let tac',t'' = negate p t' in
        tac @ tac', t''
    | Kapp(Z_of_nat,[t']) -> default true t'
@@ -1085,7 +1098,7 @@ let replay_history tactic_normalisation =
 	  let p_initial = [P_APP 2;P_TYPE] in
 	  let tac = shuffle_cancel p_initial e1.body in
 	  let solve_le =
-            let not_sup_sup = mkApp (Universes.constr_of_global (build_coq_eq ()),
+            let not_sup_sup = mkApp (Lazy.force coq_eq,
 				     [|
 					Lazy.force coq_comparison;
 					Lazy.force coq_Gt;
@@ -1245,7 +1258,7 @@ let replay_history tactic_normalisation =
 	  and eq2 = val_of(decompile orig) in
 	  let vid = unintern_id v in
 	  let theorem =
-            mkApp (build_coq_ex (), [|
+            mkApp (Lazy.force coq_ex, [|
 		      Lazy.force coq_Z;
 		      mkLambda
 			(Name vid,
@@ -1356,15 +1369,15 @@ let replay_history tactic_normalisation =
   in
   loop
 
-let normalize p_initial t =
-  let (tac,t') = transform p_initial t in
+let normalize sigma p_initial t =
+  let (tac,t') = transform sigma p_initial t in
   let (tac',t'') = condense p_initial t' in
   let (tac'',t''') = clear_zero p_initial t'' in
   tac @ tac' @ tac'' , t'''
 
-let normalize_equation id flag theorem pos t t1 t2 (tactic,defs) =
+let normalize_equation sigma id flag theorem pos t t1 t2 (tactic,defs) =
   let p_initial = [P_APP pos ;P_TYPE] in
-  let (tac,t') = normalize p_initial t in
+  let (tac,t') = normalize sigma p_initial t in
   let shift_left =
     tclTHEN
       (Proofview.V82.of_tactic (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ]))
@@ -1378,35 +1391,39 @@ let normalize_equation id flag theorem pos t t1 t2 (tactic,defs) =
   else
     (tactic,defs)
 
+let pf_nf gl c = Tacmach.New.pf_apply Tacred.simpl gl c
+
 let destructure_omega gl tac_def (id,c) =
+  let open Tacmach.New in
+  let sigma = project gl in
   if String.equal (atompart_of_id id) "State" then
     tac_def
   else
-    try match destructurate_prop c with
+    try match destructurate_prop sigma c with
       | Kapp(Eq,[typ;t1;t2])
-	when begin match destructurate_type (pf_nf gl typ) with Kapp(Z,[]) -> true | _ -> false end ->
+	when begin match destructurate_type sigma (pf_nf gl typ) with Kapp(Z,[]) -> true | _ -> false end ->
 	  let t = mk_plus t1 (mk_inv t2) in
-	  normalize_equation
+	  normalize_equation sigma
 	    id EQUA (Lazy.force coq_Zegal_left) 2 t t1 t2 tac_def
       | Kapp(Zne,[t1;t2]) ->
 	  let t = mk_plus t1 (mk_inv t2) in
-	  normalize_equation
+	  normalize_equation sigma
 	    id DISE (Lazy.force coq_Zne_left) 1 t t1 t2 tac_def
       | Kapp(Zle,[t1;t2]) ->
 	  let t = mk_plus t2 (mk_inv t1) in
-	  normalize_equation
+	  normalize_equation sigma
 	    id INEQ (Lazy.force coq_Zle_left) 2 t t1 t2 tac_def
       | Kapp(Zlt,[t1;t2]) ->
 	  let t = mk_plus (mk_plus t2 (mk_integer negone)) (mk_inv t1) in
-	  normalize_equation
+	  normalize_equation sigma
 	    id INEQ (Lazy.force coq_Zlt_left) 2 t t1 t2 tac_def
       | Kapp(Zge,[t1;t2]) ->
 	  let t = mk_plus t1 (mk_inv t2) in
-	  normalize_equation
+	  normalize_equation sigma
 	    id INEQ (Lazy.force coq_Zge_left) 2 t t1 t2 tac_def
       | Kapp(Zgt,[t1;t2]) ->
 	  let t = mk_plus (mk_plus t1 (mk_integer negone)) (mk_inv t2) in
-	  normalize_equation
+	  normalize_equation sigma
 	    id INEQ (Lazy.force coq_Zgt_left) 2 t t1 t2 tac_def
       | _ -> tac_def
     with e when catchable_exception e -> tac_def
@@ -1419,10 +1436,10 @@ let reintroduce id =
 open Proofview.Notations
 
 let coq_omega =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   clear_constr_tables ();
   let hyps_types = Tacmach.New.pf_hyps_types gl in
-  let destructure_omega = Tacmach.New.of_old destructure_omega gl in
+  let destructure_omega = destructure_omega gl in
   let tactic_normalisation, system =
     List.fold_left destructure_omega ([],[]) hyps_types in
   let prelude,sys =
@@ -1472,10 +1489,11 @@ let coq_omega =
 let coq_omega = coq_omega
 
 let nat_inject =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let is_conv = Tacmach.New.pf_apply Reductionops.is_conv gl in
   let rec explore p t : unit Proofview.tactic =
-    try match destructurate_term t with
+    Proofview.tclEVARMAP >>= fun sigma ->
+    try match destructurate_term sigma t with
       | Kapp(Plus,[t1;t2]) ->
           Tacticals.New.tclTHENLIST [
 	    Proofview.V82.tactic (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2))
@@ -1511,14 +1529,14 @@ let nat_inject =
 	    ]
       | Kapp(S,[t']) ->
           let rec is_number t =
-            try match destructurate_term t with
+            try match destructurate_term sigma t with
 		Kapp(S,[t]) -> is_number t
               | Kapp(O,[]) -> true
               | _ -> false
             with e when catchable_exception e -> false
 	  in
           let rec loop p t : unit Proofview.tactic =
-            try match destructurate_term t with
+            try match destructurate_term sigma t with
 		Kapp(S,[t]) ->
                   (Tacticals.New.tclTHEN
                      (Proofview.V82.tactic (clever_rewrite_gen p
@@ -1544,7 +1562,8 @@ let nat_inject =
   and loop = function
     | [] -> Proofview.tclUNIT ()
     | (i,t)::lit ->
-	  begin try match destructurate_prop t with
+        Proofview.tclEVARMAP >>= fun sigma ->
+	  begin try match destructurate_prop sigma t with
               Kapp(Le,[t1;t2]) ->
 		Tacticals.New.tclTHENLIST [
 		  (generalize_tac
@@ -1641,7 +1660,8 @@ let not_binop = function
 exception Undecidable
 
 let rec decidability gl t =
-  match destructurate_prop t with
+  let open Tacmach.New in
+  match destructurate_prop (project gl) t with
     | Kapp(Or,[t1;t2]) ->
 	mkApp (Lazy.force coq_dec_or, [| t1; t2;
 		  decidability gl t1; decidability gl t2 |])
@@ -1659,7 +1679,7 @@ let rec decidability gl t =
     | Kapp(Not,[t1]) ->
         mkApp (Lazy.force coq_dec_not, [| t1; decidability gl t1 |])
     | Kapp(Eq,[typ;t1;t2]) ->
-	begin match destructurate_type (pf_nf gl typ) with
+	begin match destructurate_type (project gl) (pf_nf gl typ) with
           | Kapp(Z,[]) ->  mkApp (Lazy.force coq_dec_eq, [| t1;t2 |])
           | Kapp(Nat,[]) ->  mkApp (Lazy.force coq_dec_eq_nat, [| t1;t2 |])
           | _ -> raise Undecidable
@@ -1671,35 +1691,44 @@ let rec decidability gl t =
     | Kapp(True,[]) -> Lazy.force coq_dec_True
     | _ -> raise Undecidable
 
+let fresh_id avoid id gl =
+  fresh_id_in_env avoid id (Proofview.Goal.env gl)
+
 let onClearedName id tac =
   (* We cannot ensure that hyps can be cleared (because of dependencies), *)
   (* so renaming may be necessary *)
   Tacticals.New.tclTHEN
     (Tacticals.New.tclTRY (clear [id]))
-    (Proofview.Goal.nf_enter { enter = begin fun gl ->
-     let id = Tacmach.New.of_old (fresh_id [] id) gl in
+    (Proofview.Goal.enter { enter = begin fun gl ->
+     let id = fresh_id [] id gl in
      Tacticals.New.tclTHEN (introduction id) (tac id)
     end })
 
 let onClearedName2 id tac =
   Tacticals.New.tclTHEN
     (Tacticals.New.tclTRY (clear [id]))
-    (Proofview.Goal.nf_enter { enter = begin fun gl ->
-     let id1 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_left")) gl in
-     let id2 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_right")) gl in
+    (Proofview.Goal.enter { enter = begin fun gl ->
+     let id1 = fresh_id [] (add_suffix id "_left") gl in
+     let id2 = fresh_id [] (add_suffix id "_right") gl in
       Tacticals.New.tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ]
     end })
 
+let rec is_Prop sigma c = match EConstr.kind sigma c with
+  | Sort (Prop Null) -> true
+  | Cast (c,_,_) -> is_Prop sigma c
+  | _ -> false
+
 let destructure_hyps =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let type_of = Tacmach.New.pf_unsafe_type_of gl in
-  let decidability = Tacmach.New.of_old decidability gl in
-  let pf_nf = Tacmach.New.of_old pf_nf gl in
+  let decidability = decidability gl in
+  let pf_nf = pf_nf gl in
     let rec loop = function
       | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega)
       | decl::lit ->
           let i = NamedDecl.get_id decl in
-	  begin try match destructurate_prop (NamedDecl.get_type decl) with
+          Proofview.tclEVARMAP >>= fun sigma ->
+	  begin try match destructurate_prop sigma (NamedDecl.get_type decl) with
 	  | Kapp(False,[]) -> elim_id i
           | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit
           | Kapp(Or,[t1;t2]) ->
@@ -1720,7 +1749,7 @@ let destructure_hyps =
           | Kimp(t1,t2) ->
 	      (* t1 and t2 might be in Type rather than Prop.
 		 For t1, the decidability check will ensure being Prop. *)
-              if is_Prop (type_of t2)
+              if is_Prop sigma (type_of t2)
               then
 		let d1 = decidability t1 in
 		Tacticals.New.tclTHENLIST [
@@ -1732,7 +1761,7 @@ let destructure_hyps =
               else
 		loop lit
           | Kapp(Not,[t]) ->
-              begin match destructurate_prop t with
+              begin match destructurate_prop sigma t with
 		Kapp(Or,[t1;t2]) ->
                   Tacticals.New.tclTHENLIST [
 		    (generalize_tac
@@ -1789,7 +1818,7 @@ let destructure_hyps =
 		   with Not_found -> loop lit)
 	      | Kapp(Eq,[typ;t1;t2]) ->
                   if !old_style_flag then begin
-		    match destructurate_type (pf_nf typ) with
+		    match destructurate_type sigma (pf_nf typ) with
 		    | Kapp(Nat,_) ->
                         Tacticals.New.tclTHENLIST [
 			  (simplest_elim
@@ -1806,7 +1835,7 @@ let destructure_hyps =
                         ]
 		    | _ -> loop lit
                   end else begin
-		    match destructurate_type (pf_nf typ) with
+		    match destructurate_type sigma (pf_nf typ) with
 		    | Kapp(Nat,_) ->
                         (Tacticals.New.tclTHEN
 			   (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|]))
@@ -1832,11 +1861,14 @@ let destructure_hyps =
   end }
 
 let destructure_goal =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
-    let decidability = Tacmach.New.of_old decidability gl in
+    let decidability = decidability gl in
     let rec loop t =
-      match destructurate_prop t with
+      Proofview.tclEVARMAP >>= fun sigma ->
+      let prop () = Proofview.tclUNIT (destructurate_prop sigma t) in
+      Proofview.V82.wrap_exceptions prop >>= fun prop ->
+      match prop with
       | Kapp(Not,[t]) ->
           (Tacticals.New.tclTHEN
 	     (Tacticals.New.tclTHEN (unfold sp_not) intro)
@@ -1851,7 +1883,7 @@ let destructure_goal =
                 (Proofview.V82.tactic (Tacmach.refine
 		                         (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |]))))
 	        intro
-	    with Undecidable -> Tactics.elim_type (build_coq_False ())
+	    with Undecidable -> Tactics.elim_type (Lazy.force coq_False)
 	  in
 	  Tacticals.New.tclTHEN goal_tac destructure_hyps
     in