Suppression de Abst

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

5 files changed, 25 insertions, 22 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index c301b62d11..f325621820 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -464,7 +464,7 @@ let descend_then sigma env head dirn =
 	let result = if i = dirn then dirnval else dfltval in
 	it_mkLambda_or_LetIn_name env result cstr.(i-1).cs_args
       in
-      mkMutCase (make_default_case_info mispec, p, head,
+      mkMutCaseL (make_default_case_info mispec, p, head,
 		 List.map build_branch (interval 1 (mis_nconstr mispec)))))
   
 (* Now we need to construct the discriminator, given a discriminable
@@ -509,7 +509,7 @@ let construct_discriminator sigma env dirn c sort =
     it_mkLambda_or_LetIn endpt cstrs.(i-1).cs_args 
   in
   let build_match =
-    mkMutCase (make_default_case_info mispec, p, c,
+    mkMutCaseL (make_default_case_info mispec, p, c,
 	       List.map build_branch (interval 1 (mis_nconstr mispec)))
   in
   build_match
diff --git a/tactics/refine.ml b/tactics/refine.ml
index f188eba7f5..f5a95d59c1 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -124,7 +124,7 @@ let fresh env n =
 
 let rec compute_metamap env c = match kind_of_term c with
   (* le terme est directement une preuve *)
-  | (IsConst _ | IsEvar _ | IsAbst _ | IsMutInd _ | IsMutConstruct _ |
+  | (IsConst _ | IsEvar _ | IsMutInd _ | IsMutConstruct _ |
     IsSort _ | IsVar _ | IsRel _) -> TH (c,[],[])
 
   (* le terme est une mv => un but *)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 87a4370cb6..b77ac413c8 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -297,9 +297,9 @@ let general_elim_then_using
   elim elim_sign_fun tac predicate (indbindings,elimbindings) c gl =
   let ((ity,_,_),t) = reduce_to_ind_goal gl (pf_type_of gl c) in
   let name_elim =
-    (match elim with
-       | DOPN(Const sp,_) -> id_of_string(string_of_path sp)
-       | VAR id -> id
+    (match kind_of_term elim with
+       | IsConst (sp,_) -> id_of_string (string_of_path sp)
+       | IsVar id -> id
        | _ -> id_of_string " ") 
   in
   (* applying elimination_scheme just a little modified *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3b24ad75d1..4312071b48 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -40,6 +40,7 @@ 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
@@ -48,18 +49,18 @@ let force_reference c =
   | DOPN (MutInd (sp,i),ctxt) -> c
   | VAR id -> c
   | _ -> error "Not an atomic type"
+*)
 
-let rec string_head_bound = function 
-  | DOPN(Const _,_) as x -> 
-      string_of_id (basename (path_of_const x))
-  | DOPN(MutInd ind_sp,args) as x -> 
+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) -> 
       let mispec = Global.lookup_mind_specif (ind_sp,args) in 
       string_of_id (mis_typename mispec)
-  |  DOPN(MutConstruct (ind_sp,i),args) ->
+  | IsMutConstruct ((ind_sp,i),args) ->
        let mispec = Global.lookup_mind_specif (ind_sp,args) in 
        string_of_id (mis_consnames mispec).(i-1)
-  |  VAR id -> string_of_id id
-  |  _ -> raise Bound
+  | IsVar id -> string_of_id id
+  | _ -> raise Bound
 
 let string_head c = 
   try string_head_bound c with Bound -> error "Bound head variable"
@@ -232,10 +233,10 @@ let dyn_reduce = function
 (* Unfolding occurrences of a constant *)
 
 let unfold_constr c = 
-  match strip_outer_cast c with 
-    | DOPN(Const(sp),_) -> 
+  match kind_of_term (strip_outer_cast c) with 
+    | IsConst(sp,_) -> 
 	unfold_in_concl [[],sp]
-    | t -> 
+    | _ -> 
 	errorlabstrm "unfold_constr"
 	  [< 'sTR "Cannot unfold a non-constant." >]
 
@@ -937,14 +938,14 @@ let dyn_split  = function
  * gl : the current goal
 *)
 
-let last_arg = function
-  | DOPN(AppL,cl) ->  cl.(Array.length cl - 1)
+let last_arg c = match kind_of_term c with
+  | IsAppL (f,cl) ->  List.nth cl (List.length cl - 1)
   | _ -> anomaly "last_arg"
 	
 let elimination_clause_scheme kONT wc elimclause indclause gl = 
   let indmv = 
-    (match last_arg (clenv_template elimclause).rebus with
-       | DOP0(Meta mv) -> mv
+    (match kind_of_term (last_arg (clenv_template elimclause).rebus) with
+       | IsMeta mv -> mv
        | _  -> errorlabstrm "elimination_clause"
              [< 'sTR "The type of elimination clause is not well-formed" >]) 
   in
@@ -1416,8 +1417,8 @@ let dyn_destruct = function
 let elim_scheme_type elim t gl =
   let (wc,kONT) = startWalk gl in
   let clause = mk_clenv_type_of wc elim in 
-  match last_arg (clenv_template clause).rebus with
-    | DOP0(Meta mv) ->
+  match kind_of_term (last_arg (clenv_template clause).rebus) with
+    | IsMeta mv ->
         let clause' = clenv_unify (clenv_instance_type clause mv) t clause in 
 	elim_res_pf kONT clause' gl
     | _ -> anomaly "elim_scheme_type"
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 92e76fbd3d..25fabac03e 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -26,7 +26,9 @@ val type_clenv_binding : walking_constraints ->
   constr * constr -> constr substitution  -> constr
 
 (* [force_reference c] fails if [c] is not a reference *)
+(*
 val force_reference   : constr -> constr
+*)
 
 val string_head       : constr -> string
 val head_constr       : constr -> constr list