Modification mkAppL; abstraction via kind_of_term; changement dans Reduction

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@597 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 122 insertions, 111 deletions

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 09d8885d83..bad9866f63 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -92,13 +92,10 @@ let instantiate_tac = function
       (fun gl -> instantiate n (pf_interp_constr gl com) gl)
   | _ -> invalid_arg "Instantiate called with bad arguments"
 
-let whd_evar env sigma = function
-  | DOPN(Evar n, cl) as k ->
-      if Evd.in_dom sigma n & Evd.is_defined sigma n then
+let whd_evar env sigma c = match kind_of_term c with
+  | IsEvar (n, cl) when Evd.in_dom sigma n & Evd.is_defined sigma n ->
         Instantiate.existential_value sigma (n,cl)
-      else 
-	k
-  | x -> x
+  | _ -> c
 
 let normEvars gl =
   let sigma = project gl in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index bec81d44a8..2b9b230115 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -172,8 +172,9 @@ let v_conditional_rewriteRL =
    is substitutive *)
 
 let find_constructor env sigma c =
-  match whd_betadeltaiota_stack env sigma c [] with
-    | DOPN(MutConstruct _,_) as hd,stack -> (hd,stack)
+  let hd,stack = whd_betadeltaiota_stack env sigma c in
+  match kind_of_term hd with
+    | IsMutConstruct _ -> (hd,stack)
     | _ -> error "find_constructor"
 
 type leibniz_eq = {
@@ -342,8 +343,8 @@ exception DiscrFound of (sorts oper * int) list * sorts oper * sorts oper
 
 let find_positions env sigma t1 t2 =
   let rec findrec posn t1 t2 =
-    match (whd_betadeltaiota_stack env sigma t1 [],
-           whd_betadeltaiota_stack env sigma t2 []) with
+    match (whd_betadeltaiota_stack env sigma t1,
+           whd_betadeltaiota_stack env sigma t2) with
   	
       | ((DOPN(MutConstruct sp1 as oper1,_) as hd1,args1),
 	 (DOPN(MutConstruct sp2 as oper2,_) as hd2,args2)) ->
@@ -527,8 +528,8 @@ let rec build_discriminator sigma env dirn c sort = function
       let subval = build_discriminator sigma cnum_env dirn newc sort l  in
       (match necessary_elimination arsort (destSort sort) with
          | Type_Type ->
-	     kont subval (build_EmptyT (),DOP0(Sort(Type(dummy_univ))))
-	 | _ -> kont subval (build_False (),DOP0(Sort(Prop Null))))
+	     kont subval (build_EmptyT (),mkSort (Type(dummy_univ)))
+	 | _ -> kont subval (build_False (),mkSort (Prop Null)))
   | _ -> assert false
 
 let find_eq_data_decompose eqn =
@@ -615,7 +616,7 @@ let discr id gls =
 	 in
 	 tclCOMPLETE((tclTHENS (cut_intro absurd_term)
 			([onLastHyp (compose gen_absurdity out_some);
-			  refine (mkAppL [| pf; VAR id |])]))) gls
+			  refine (mkAppL (pf, [| VAR id |]))]))) gls
      | _ -> assert false)
 
 let not_found_message id =
@@ -774,11 +775,11 @@ let sig_clausale_forme env sigma sort_of_ty siglen ty (dFLT,dFLTty) =
       in
       (bindings,dFLT)
     else
-      let (a,p) = match whd_beta_stack ty [] with
+      let (a,p) = match whd_beta_stack ty with
 	| (_,[a;p]) -> (a,p)
  	| _ -> anomaly "sig_clausale_forme: should be a sigma type" in
       let mv = new_meta() in
-      let rty = applist(p,[DOP0(Meta mv)]) in
+      let rty = applist(p,[mkMeta mv]) in
       let (bindings,tuple_tail) = sigrec_clausale_forme (siglen-1) rty in
       let w =
 	try List.assoc mv bindings
@@ -958,7 +959,7 @@ let decompEqThen ntac id gls =
 	 tclCOMPLETE
 	   ((tclTHENS (cut_intro absurd_term)
 	       ([onLastHyp (compose gen_absurdity out_some);
-		 refine (mkAppL [| pf; VAR id |])]))) gls
+		 refine (mkAppL (pf, [| VAR id |]))]))) gls
      | Inr posns ->
 	 (let e = pf_get_new_id (id_of_string "e") gls in
 	  let e_env =
@@ -1041,7 +1042,7 @@ let swapEquandsInConcl gls =
     with _-> errorlabstrm "SwapEquandsInConcl" (rewrite_msg None) 
   in
   let sym_equal = get_squel lbeq.sym in
-  refine (applist(sym_equal,[t;e2;e1;DOP0(Meta(new_meta()))])) gls
+  refine (applist(sym_equal,[t;e2;e1;mkMeta (new_meta())])) gls
 
 let swapEquandsInHyp id gls =
   ((tclTHENS (cut_replacing id (swap_equands gls (clause_type (Some id) gls)))
@@ -1054,9 +1055,9 @@ let swapEquandsInHyp id gls =
    otherwise *)
 
 let find_elim  sort_of_gl  lbeq =
-  match  sort_of_gl  with
-    | DOP0(Sort(Prop Null))  (* Prop *)  ->  (get_squel lbeq.ind, false)  
-    | DOP0(Sort(Prop Pos))   (* Set *)   ->  
+  match kind_of_term sort_of_gl  with
+    | IsSort(Prop Null)  (* Prop *)  ->  (get_squel lbeq.ind, false)  
+    | IsSort(Prop Pos)   (* Set *)   ->  
 	(match lbeq.rrec with
            | Some eq_rec -> (get_squel eq_rec, false) 
 	   | None -> errorlabstrm "find_elim"
@@ -1100,8 +1101,8 @@ let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
     else
       (build_non_dependent_rewrite_predicate (t,e1,e2)  body  gls)
   in
-  refine (applist(eq_elim,[t;e1;p;DOP0(Meta(new_meta()));
-                           e2;DOP0(Meta(new_meta()))])) gls
+  refine (applist(eq_elim,[t;e1;p;mkMeta(new_meta());
+                           e2;mkMeta(new_meta())])) gls
 
 (* [subst_tuple_term dep_pair B]
 
@@ -1169,6 +1170,27 @@ let decomp_tuple_term env c t =
   in
   List.split (decomprec (Rel 1) c t)
 
+(*
+let whd_const_state namelist env sigma = 
+  let rec whrec (x, l as s) =
+    match kind_of_term x with
+      | IsConst (sp,_) when List.mem sp namelist ->
+          if evaluable_constant env x then
+            whrec (constant_value env x, l)
+          else 
+	    error "whd_const_stack"
+      | IsCast (c,_) -> whrec (c, l)
+      | IsAppL (f,cl) -> whrec (f, append_stack cl l)
+      | _ -> s
+  in 
+  whrec
+let whd_const_state namelist = whd_state (const namelist)
+let whd_const_stack namelist env sigma x =
+  whd_const_state namelist env sigma (x, empty_stack)
+let whd_const namelist env sigma c = 
+  app_stack (whd_const_stack namelist env sigma (c, empty_stack))
+*)
+
 let subst_tuple_term env sigma dep_pair b =
   let typ = get_type_of env sigma dep_pair in
   let e_list,proj_list = decomp_tuple_term env dep_pair typ in
@@ -1291,7 +1313,7 @@ let rec eq_mod_rel l_meta t0 t1 =
 let is_hd_const c = match kind_of_term c with
   | IsAppL (f,args) ->
       (match kind_of_term f with
-         | IsConst (c,_) -> Some (c, Array.of_list args)
+         | IsConst (c,_) -> Some (c, args)
          |_ -> None)
   | _ -> None
 
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 08105aa9f0..ce60df06a1 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -88,7 +88,7 @@ let replace_by_meta env = function
   | TH (m, mm, sgp) when isMeta (strip_outer_cast m) -> m,mm,sgp
   | (TH (c,mm,_)) as th ->
       let n = new_meta() in
-      let m = DOP0(Meta n) in
+      let m = mkMeta n in
       (* quand on introduit une mv on calcule son type *)
       let ty = match kind_of_term c with
 	| IsLambda (Name id,c1,c2) when isCast c2 ->
@@ -131,7 +131,7 @@ let rec compute_metamap env c = match kind_of_term c with
   | IsMeta n ->
       Pp.warning (Printf.sprintf ("compute_metamap: MV(%d) sans type !\n") n);
       TH (c,[],[None])
-  | IsCast (DOP0(Meta n),ty) -> TH (c,[n,ty],[None])
+  | IsCast (m,ty) when isMeta m -> TH (c,[destMeta m,ty],[None])
 
   (* abstraction => il faut décomposer si le terme dessous n'est pas pur
    *    attention : dans ce cas il faut remplacer (Rel 1) par (VAR x)
@@ -154,10 +154,10 @@ let rec compute_metamap env c = match kind_of_term c with
 
   (* 4. Application *)
   | IsAppL (f,v) ->
-      let a = Array.map (compute_metamap env) (Array.of_list (f::v)) in
+      let a = Array.map (compute_metamap env) (Array.append [|f|] v) in
       begin
 	try
-	  let v',mm,sgp = replace_in_array env a in TH (mkAppL v',mm,sgp)
+	  let v',mm,sgp = replace_in_array env a in TH (mkAppA v',mm,sgp)
 	with NoMeta ->
 	  TH (c,[],[])
       end
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index d5ee7f9659..feb48e4ef9 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -52,7 +52,7 @@ let tclMAP tacfun l =
 (* apply a tactic to the nth element of the signature  *)
 
 let tclNTH_HYP m (tac : constr->tactic) gl =
-  tac (try VAR(let (id,_,_) = List.nth (pf_hyps gl) (m-1) in id) 
+  tac (try mkVar(let (id,_,_) = List.nth (pf_hyps gl) (m-1) in id) 
        with Failure _ -> error "No such assumption") gl
 
 (* apply a tactic to the last element of the signature  *)
@@ -62,8 +62,8 @@ let tclLAST_HYP = tclNTH_HYP 1
 let tclTRY_sign (tac : constr->tactic) sign gl =
   let rec arec = function
     | []      -> tclFAIL 0
-    | [s]     -> tac (VAR(s)) (* added in order to get useful error messages *)
-    | (s::sl) -> tclORELSE (tac (VAR(s))) (arec sl) 
+    | [s]     -> tac (mkVar s) (*added in order to get useful error messages *)
+    | (s::sl) -> tclORELSE (tac (mkVar s)) (arec sl) 
   in 
   arec (ids_of_var_context sign) gl
 
@@ -281,16 +281,16 @@ let elim_sign ity i =
   analrec [] recarg.(i-1)
 
 let sort_of_goal gl = 
-  match hnf_type_of gl (pf_concl gl) with 
-    | DOP0(Sort s) -> s
-    | _            -> anomaly "goal should be a type"
+  match kind_of_term (hnf_type_of gl (pf_concl gl)) with 
+    | IsSort s -> s
+    | _        -> anomaly "goal should be a type"
 
 
 (* 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 last_arg c = match kind_of_term c with
-  | IsAppL (f,cl) -> List.nth cl (List.length cl - 1)
+  | IsAppL (f,cl) -> array_last cl
   | _ -> anomaly "last_arg"
 
 let general_elim_then_using 
@@ -312,9 +312,10 @@ let general_elim_then_using
       | IsMeta mv -> mv
       | _         -> error "elimination"
   in
-  let pmv = 
-    match decomp_app (clenv_template_type elimclause).rebus with
-      | (DOP0(Meta(p)),oplist) -> p
+  let pmv =
+    let p, _ = decomp_app (clenv_template_type elimclause).rebus in
+    match kind_of_term p with
+      | IsMeta p -> p
       | _ -> error ("The elimination combinator " ^
                     (string_of_id name_elim) ^ " is not known") 
   in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a8693a70be..60ea7e8d07 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -40,17 +40,6 @@ let get_pairs_from_bindings =
   in 
   List.map pair_from_binding
 
-(*
-let force_reference c =
-  match fst (decomp_app c) with
-  | DOPN (Const sp,ctxt) -> c
-  | DOPN (Evar ev,ctxt) -> c
-  | DOPN (MutConstruct (spi,j),ctxt) -> c
-  | DOPN (MutInd (sp,i),ctxt) -> c
-  | VAR id -> c
-  | _ -> error "Not an atomic type"
-*)
-
 let rec string_head_bound x = match kind_of_term x with
   | IsConst _ -> string_of_id (basename (path_of_const x))
   | IsMutInd (ind_sp,args) -> 
@@ -70,7 +59,8 @@ let rec head_constr_bound t l =
   let t = strip_outer_cast(collapse_appl t) in
   match kind_of_term t with
     | IsProd (_,_,c2)  -> head_constr_bound c2 l 
-    | IsAppL (f,args)  -> head_constr_bound f (args@l)
+    | IsAppL (f,args)  -> 
+	head_constr_bound f (Array.fold_right (fun a l -> a::l) args l)
     | IsConst _        -> t::l
     | IsMutInd _       -> t::l
     | IsMutConstruct _ -> t::l
@@ -155,8 +145,8 @@ let reduct_in_concl redfun gl =
     
 let reduct_in_hyp redfun id gl  = 
   let ty = pf_get_hyp_typ gl id in
-  let redfun' = under_casts (fun _ _ -> pf_reduce redfun gl) in
-  convert_hyp id (redfun' (pf_env gl) (project gl) ty) gl
+  let redfun' = under_casts (pf_reduce redfun gl) in
+  convert_hyp id (redfun' ty) gl
     
 let reduct_option redfun = function
   | Some id -> reduct_in_hyp   redfun id 
@@ -271,9 +261,9 @@ let id_of_name_with_default s = function
 let default_id gl =
   match kind_of_term (strip_outer_cast (pf_concl gl)) with
     | IsProd (name,c1,c2) ->
-  	(match pf_whd_betadeltaiota gl (pf_type_of gl c1) with
-	   | DOP0(Sort(Prop _))  -> (id_of_name_with_default "H" name)
-	   | DOP0(Sort(Type(_))) -> (id_of_name_with_default "X" name)
+  	(match kind_of_term (pf_whd_betadeltaiota gl (pf_type_of gl c1)) with
+	   | IsSort (Prop _) -> (id_of_name_with_default "H" name)
+	   | IsSort (Type _) -> (id_of_name_with_default "X" name)
 	   | _                   -> anomaly "Wrong sort")
     | _ -> error "Introduction needs a product"
 
@@ -466,10 +456,10 @@ let bring_hyps clsl gl =
          | None      -> error "BringHyps") clsl in
   let newcl = 
     List.fold_right 
-      (fun id cl' -> mkNamedProd id (pf_type_of gl (VAR id)) cl')
+      (fun id cl' -> mkNamedProd id (pf_type_of gl (mkVar id)) cl')
       ids (pf_concl gl)
   in 
-  apply_type newcl (List.map (fun id -> VAR id) ids) gl
+  apply_type newcl (List.map mkVar ids) gl
 
 (* Resolution with missing arguments *)
 
@@ -535,7 +525,7 @@ let cut_and_apply c gl =
     | IsProd (_,c1,c2) when not (dependent (mkRel 1) c2) ->
 	tclTHENS 
 	  (apply_type (mkProd (Anonymous,c2,goal_constr))
-	     [DOP0(Meta(new_meta()))])
+	     [mkMeta (new_meta())])
 	  [tclIDTAC;apply_term c [mkMeta (new_meta())]] gl
     | _ -> error "Imp_elim needs a non-dependent product"
 
@@ -549,8 +539,8 @@ let dyn_cut_and_apply = function
 (**************************)
 
 let cut c gl =
-  match hnf_type_of gl c with
-    | (DOP0(Sort _)) ->
+  match kind_of_term (hnf_type_of gl c) with
+    | IsSort _ ->
 	apply_type (mkProd (Anonymous, c, pf_concl gl)) 
           [mkMeta (new_meta())] gl
     | _  -> error "Not a proposition or a type"
@@ -582,8 +572,8 @@ let cut_in_parallel l =
 
 let generalize_goal gl c cl =
   let t = pf_type_of gl c in
-  match c with
-    | (VAR id) -> mkNamedProd id t cl
+  match kind_of_term c with
+    | IsVar id -> mkNamedProd id t cl
     | _        -> 
         let cl' = subst_term c cl in 
         if noccurn 1 cl' then 
@@ -608,8 +598,8 @@ let generalize_dep c gl =
   let qhyps = List.map (fun (id,_,_) -> id) to_quantify in
   let tothin = List.filter (fun id -> not (List.mem id init_ids)) qhyps in
   let tothin' =
-    match c with
-      | VAR id when mem_var_context id sign & not (List.mem id init_ids)
+    match kind_of_term c with
+      | IsVar id when mem_var_context id sign & not (List.mem id init_ids)
 	  -> id::tothin
       | _ -> tothin
   in
@@ -618,7 +608,7 @@ let generalize_dep c gl =
       (fun c d -> mkNamedProd_or_LetIn d c) (pf_concl gl) to_quantify in
   let cl'' = generalize_goal gl c cl' in
   tclTHEN
-    (apply_type cl'' (c::(List.map (fun id -> VAR id) qhyps)))
+    (apply_type cl'' (c::(List.map mkVar qhyps)))
     (thin (List.rev tothin'))
     gl
     
@@ -670,7 +660,7 @@ let letin_abstract id c occ_ccl occ_hyps gl =
   let abstract ((depdecls,marks,occl as accu),lhyp) (hyp,bodyopt,typ as d) =
     try 
       let occ = if allhyp then [] else List.assoc hyp occl in
-      let newdecl = subst1 (VAR id) (subst_term_occ_decl occ c d) in
+      let newdecl = subst1 (mkVar id) (subst_term_occ_decl occ c d) in
       let newoccl = list_except_assoc hyp occl in
       if d=newdecl then
 	(accu,Some hyp)
@@ -689,7 +679,7 @@ let letin_abstract id c occ_ccl occ_hyps gl =
   end;
   let ccl = match occ_ccl with
     | None -> (pf_concl gl)
-    | Some occ -> subst1 (VAR id) (subst_term_occ occ c (pf_concl gl)) 
+    | Some occ -> subst1 (mkVar id) (subst_term_occ occ c (pf_concl gl)) 
   in
   (depdecls,marks,ccl)
 
@@ -710,10 +700,10 @@ let letin_tac with_eq name c occ_ccl occ_hyps gl =
   in
   let heq = next_global_ident_away (id_of_string "Heq") (ids_of_sign hyps) in
   let tmpcl = List.fold_right mkNamedProd_or_LetIn depdecls ccl in
-  let tmpargs = List.map (fun (id,_,_) -> VAR id) depdecls in
+  let tmpargs = List.map (fun (id,_,_) -> mkVar id) depdecls in
   let newcl,args =
     if with_eq then
-      let eq = applist (eqc,[t;VAR id;c]) in
+      let eq = applist (eqc,[t;mkVar id;c]) in
       let refl = applist (reflc,[t;c]) in
       (mkNamedProd id t (mkNamedProd heq eq tmpcl), c::refl::tmpargs)
     else
@@ -769,7 +759,7 @@ let (assumption : tactic) = fun gl ->
   let rec arec = function
     | [] -> error "No such assumption"
     | (id,c,t)::rest -> 
-	if pf_conv_x_leq gl (body_of_type t) concl then refine (VAR id) gl
+	if pf_conv_x_leq gl (body_of_type t) concl then refine (mkVar id) gl
 	else arec rest
   in
   arec (pf_hyps gl)
@@ -939,7 +929,7 @@ let dyn_split  = function
 *)
 
 let last_arg c = match kind_of_term c with
-  | IsAppL (f,cl) ->  List.nth cl (List.length cl - 1)
+  | IsAppL (f,cl) ->  array_last cl
   | _ -> anomaly "last_arg"
 	
 let elimination_clause_scheme kONT wc elimclause indclause gl = 
@@ -1098,21 +1088,21 @@ let atomize_param_of_ind hyp0 gl =
     if i<>nparams then 
       let tmptyp0 = pf_get_hyp_typ gl hyp0 in
       let (_,indtyp,_) = pf_reduce_to_mind gl tmptyp0 in
-      match (destAppL (whd_castapp indtyp)).(i) with
-	| VAR id when not (List.exists (occur_var id) avoid) ->
-	    atomize_one (i-1) ((VAR id)::avoid) gl
-	| VAR id ->
+      match kind_of_term (destAppL (whd_castapp indtyp)).(i) with
+	| IsVar id when not (List.exists (occur_var id) avoid) ->
+	    atomize_one (i-1) ((mkVar id)::avoid) gl
+	| IsVar id ->
 	    let x = fresh_id [] id gl in
 	    tclTHEN
-	      (letin_tac true (Name x) (VAR id) (Some []) [])
-	      (atomize_one (i-1) ((VAR x)::avoid)) gl
+	      (letin_tac true (Name x) (mkVar id) (Some []) [])
+	      (atomize_one (i-1) ((mkVar x)::avoid)) gl
 	| c ->
 	    let id = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c)
 		       Anonymous in
 	    let x = fresh_id [] id gl in
 	    tclTHEN
 	      (letin_tac true (Name x) c (Some []) [])
-	      (atomize_one (i-1) ((VAR x)::avoid)) gl
+	      (atomize_one (i-1) ((mkVar x)::avoid)) gl
     else 
       tclIDTAC gl
   in
@@ -1126,8 +1116,8 @@ let find_atomic_param_of_ind mind indtyp =
   let params = list_firstn nparams argl in
   let indvars = ref Idset.empty in
   for i = nparams to (Array.length argv)-1 do
-    match argv.(i) with
-      | VAR id when not (List.exists (occur_var id) params) -> 
+    match kind_of_term argv.(i) with
+      | IsVar id when not (List.exists (occur_var id) params) -> 
 	  indvars := Idset.add id !indvars
       | _ -> ()
   done;
@@ -1269,7 +1259,7 @@ let cook_sign hyp0 indvars sign =
 *)
 
 let induction_tac varname typ (elimc,elimt) gl =
-  let c = VAR varname in
+  let c = mkVar varname in
   let (wc,kONT)  = startWalk gl                    in
   let indclause  = make_clenv_binding wc (c,typ) []  in
   let elimclause = make_clenv_binding wc (mkCast (elimc,elimt),elimt) [] in
@@ -1305,7 +1295,7 @@ let induction_from_context hyp0 gl =
   let tmpcl = List.fold_right2 mkNamedProd dephyps deptyps (pf_concl gl) in
   let lc = get_constructors hyp0 (elimc,elimt) mind mindpath in
   tclTHENLIST
-    [ apply_type tmpcl (List.map (fun id -> VAR id) dephyps);
+    [ apply_type tmpcl (List.map mkVar dephyps);
       thin dephyps;
       tclTHENS
        	(tclTHEN
@@ -1320,8 +1310,8 @@ let induction_with_atomization_of_ind_arg hyp0 =
     (induction_from_context hyp0)
 
 let new_induct c gl =
-  match c with
-    | (VAR id) when not (List.mem id (ids_of_sign (Global.var_context()))) ->
+  match kind_of_term c with
+    | IsVar id when not (List.mem id (ids_of_sign (Global.var_context()))) ->
 	tclORELSE
 	  (tclTHEN (intros_until id) (tclLAST_HYP simplest_elim))
 	  (induction_with_atomization_of_ind_arg id) gl
@@ -1469,7 +1459,7 @@ let dyn_case_type = function
 let andE id gl =
   let t = pf_get_hyp_typ gl id in
   if is_conjunction (pf_hnf_constr gl t) then 
-    (tclTHEN (simplest_elim (VAR id)) (tclDO 2 intro)) gl
+    (tclTHEN (simplest_elim (mkVar id)) (tclDO 2 intro)) gl
   else 
     errorlabstrm "andE" 
       [< 'sTR("Tactic andE expects "^(string_of_id id)^" is a conjunction.")>]
@@ -1482,7 +1472,7 @@ let dAnd cls gl =
 let orE id gl =
   let t = pf_get_hyp_typ gl id in
   if is_disjunction (pf_hnf_constr gl t) then 
-    (tclTHEN (simplest_elim (VAR id)) intro) gl
+    (tclTHEN (simplest_elim (mkVar id)) intro) gl
   else 
     errorlabstrm "orE" 
       [< 'sTR("Tactic orE expects "^(string_of_id id)^" is a disjunction.")>]
@@ -1497,7 +1487,7 @@ let impE id gl =
   if is_imp_term (pf_hnf_constr gl t) then 
     let (dom, _, rng) = destProd (pf_hnf_constr gl t) in 
     (tclTHENS (cut_intro rng) 
-       [tclIDTAC;apply_term (VAR id) [DOP0(Meta(new_meta()))]]) gl
+       [tclIDTAC;apply_term (mkVar id) [mkMeta (new_meta())]]) gl
   else 
     errorlabstrm "impE"
       [< 'sTR("Tactic impE expects "^(string_of_id id)^
@@ -1517,7 +1507,7 @@ let dImp cls gl =
 let contradiction_on_hyp id gl =
   let hyp = pf_get_hyp_typ gl id in
   if is_empty_type hyp then
-    simplest_elim (VAR id) gl
+    simplest_elim (mkVar id) gl
   else 
     error "Not a contradiction"
 
@@ -1532,7 +1522,7 @@ let absurd c gls =
 	       ((fun gl ->
 		   let ida = pf_nth_hyp_id gl 1
                    and idna = pf_nth_hyp_id gl 2 in
-                   exact (applist(VAR idna,[VAR ida])) gl)));
+                   exact (applist(mkVar idna,[mkVar ida])) gl)));
             tclIDTAC]));
        tclIDTAC])) gls
 
@@ -1580,8 +1570,8 @@ let symmetry gl =
 	    (apply (pf_parse_const gl ("sym_"^hdcncls)) gl)
           with  _ ->
             let symc = match args with 
-              | [typ;c1;c2] -> mkAppL [| hdcncl; typ; c2; c1 |]
-              | [c1;c2]     -> mkAppL [| hdcncl; c2; c1 |]  
+              | [typ;c1;c2] -> mkAppL (hdcncl, [| typ; c2; c1 |])
+              | [c1;c2]     -> mkAppL (hdcncl, [| c2; c1 |])
 	      | _ -> assert false 
 	    in 
 	    (tclTHENS (cut symc)
@@ -1619,13 +1609,13 @@ let transitivity t gl =
 	    apply_list [(pf_parse_const gl ("trans_"^hdcncls));t] gl 
           with  _ -> 
             let eq1 = match args with 
-              | [typ;c1;c2] -> mkAppL [| hdcncl; typ; c1; t |]
-	      | [c1;c2]     -> mkAppL [| hdcncl; c1; t|]
+              | [typ;c1;c2] -> mkAppL (hdcncl, [| typ; c1; t |])
+	      | [c1;c2]     -> mkAppL (hdcncl, [| c1; t|])
 	      | _ -> assert false 
 	    in
             let eq2 = match args with 
-              | [typ;c1;c2] -> mkAppL [| hdcncl; typ; t; c2 |]
-	      | [c1;c2]     -> mkAppL [| hdcncl; t; c2 |]
+              | [typ;c1;c2] -> mkAppL (hdcncl, [| typ; t; c2 |])
+	      | [c1;c2]     -> mkAppL (hdcncl, [| t; c2 |])
 	      |  _ -> assert false 
 	    in
             (tclTHENS (cut eq2)
@@ -1677,7 +1667,7 @@ let abstract_subproof name tac gls =
     Declare.construct_reference newenv CCI na
   in
   exact (applist (lemme,
-		  List.map (fun id -> VAR id) (List.rev (ids_of_var_context sign))))
+		  List.map mkVar (List.rev (ids_of_var_context sign))))
     gls
 
 let tclABSTRACT name_op tac gls = 
diff --git a/tactics/tauto.ml b/tactics/tauto.ml
index 7c00a6b1d3..171eea17b6 100644
--- a/tactics/tauto.ml
+++ b/tactics/tauto.ml
@@ -81,7 +81,7 @@ let is_atomic m =
       (is_matching (get_pat pi_pattern) m)  ||
       (is_matching (not_pattern ()) m))
       
-let hypothesis = function Some id -> exact (VAR id) | None -> assert false
+let hypothesis = function Some id -> exact (mkVar id) | None -> assert false
 
 (* Steps of the procedure *)
 
@@ -205,12 +205,12 @@ B,Gamma|- G   D->B,Gamma |- C->D
 *)
 
 let back_thru_2 id =
-  applist(VAR id,[DOP0(Meta(new_meta()));DOP0(Meta(new_meta()))])
+  applist(mkVar id,[mkMeta (new_meta());mkMeta (new_meta())])
 
 let back_thru_1 id =
-  applist(VAR id,[DOP0(Meta(new_meta()))])
+  applist(mkVar id,[mkMeta(new_meta())])
 
-let exact_last_hyp = onLastHyp (fun h -> exact (VAR (out_some h)))
+let exact_last_hyp = onLastHyp (fun h -> exact (mkVar (out_some h)))
 
 let imply_imply_bot_pattern = put_pat mmk "(?1 -> ?2) -> ?3"
 
@@ -260,7 +260,7 @@ let true_imply_step cls gls =
 	  let h0 = out_some cls in  
 	  (tclTHENS (cut_intro b)
 	     [(clear_clause cls);
-	      (tclTHEN (apply(VAR h0)) (one_constructor 1 []))]) gls
+	      (tclTHEN (apply(mkVar h0)) (one_constructor 1 []))]) gls
       | _ -> anomaly "Inconsistent pattern-matching"
   with PatternMatchingFailure -> error "true_imply_step"
 	  
@@ -1765,7 +1765,7 @@ let search env id =
     Rel (fst (lookup_rel_id id (Environ.rel_context env)))
   with Not_found ->
   if mem_var_context id (Environ.var_context env) then
-    VAR id
+    mkVar id
   else
     global_reference CCI id
 
@@ -1837,11 +1837,13 @@ let cut_in_parallelUsing idlist l =
   in 
   prec (List.rev idlist) (List.rev l)
 
-let exacto tt gls = 
-  match (try cci_of_tauto_term (pf_env gls) tt with
-             _ -> (DOP0 Prod)) with (* Efectivamente, es cualquier cosa!! *)
-    | (DOP0 Prod) -> tAUTOFAIL gls  (* Esto confirma el comentario anterior *)
-    | t -> (exact t) gls
+let exacto tt gls =
+  let tac =
+    try
+      let t = cci_of_tauto_term (pf_env gls) tt in
+      exact t
+    with _ -> tAUTOFAIL     (* Efectivamente, es cualquier cosa!! *)
+  in tac gls                (* Esto confirma el comentario anterior *)
     
 let subbuts l hyp = cut_in_parallelUsing
                       (lisvar l) 
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 920e6ba310..c62746cc71 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -17,7 +17,7 @@ type 'a t = (constr_label,constr_pattern,'a) Dn.t
 
 let decomp = 
   let rec decrec acc c = match kind_of_term c with
-    | IsAppL (f,l) -> decrec (l@acc) f
+    | IsAppL (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f
     | IsCast (c1,_) -> decrec acc c1
     | _ -> (c,acc)
   in 
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index 4f071980e6..de5adc94df 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.ml
@@ -132,15 +132,14 @@ and build_term ce p_0 c =
   match p_0, kind_of_term c with 
     | ((na,Some t), IsMeta mv) -> 
 (*    	let mv = new_meta() in *)
-	(DOP0(Meta mv),
-         clenv_pose (na,mv,t) ce)
+	(mkMeta mv, clenv_pose (na,mv,t) ce)
     | ((na,_), IsCast (c,t)) -> build_term ce (na,Some t) c
     | ((na,Some t), _) ->
     	if (not((occur_meta c))) then 
 	  (c,ce)
     	else 
 	  let (hd,args) = 
-	    whd_betadeltaiota_stack env (w_Underlying ce.hook) c [] in
+	    whd_betadeltaiota_stack env (w_Underlying ce.hook) c in
           let hdty = w_type_of ce.hook hd in
           let (args,ce') =
 	    build_args [] ce (w_whd_betadeltaiota ce.hook hdty) args in
@@ -155,7 +154,7 @@ and build_term ce p_0 c =
 	  (c,ce)
     	else 
 	  let (hd,args) = 
-	    whd_betadeltaiota_stack env (w_Underlying ce.hook) c [] in
+	    whd_betadeltaiota_stack env (w_Underlying ce.hook) c in
           let hdty = w_type_of ce.hook hd in
           let (args,ce') = 
 	    build_args [] ce (w_whd_betadeltaiota ce.hook hdty) args in