Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 7 insertions, 8 deletions

diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index bda04db3..462e5ed8 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: quote.ml,v 1.30.2.1 2004/07/16 19:30:14 herbelin Exp $ *)
+(* $Id: quote.ml 7639 2005-12-02 10:01:15Z gregoire $ *)
 
 (* The `Quote' tactic *)
 
@@ -107,7 +107,6 @@ open Pp
 open Util
 open Names
 open Term
-open Instantiate
 open Pattern
 open Matching
 open Tacmach
@@ -213,7 +212,7 @@ let compute_rhs bodyi index_of_f =
 	  PMeta (Some (coerce_meta_in i))
       | App (f,args) ->
           PApp (pattern_of_constr f, Array.map aux args)
-      | Cast (c,t) -> aux c 
+      | Cast (c,_,_) -> aux c 
       | _ -> pattern_of_constr c
   in
   aux bodyi
@@ -298,7 +297,7 @@ binary search trees (see file \texttt{Quote.v}) *)
 let rec closed_under cset t =
   (ConstrSet.mem t cset) or
   (match (kind_of_term t) with
-     | Cast(c,_) -> closed_under cset c  
+     | Cast(c,_,_) -> closed_under cset c  
      | App(f,l) -> closed_under cset f & array_for_all (closed_under cset) l
      | _ -> false)
     
@@ -361,7 +360,7 @@ let rec subterm gl (t : constr) (t' : constr) =
   (pf_conv_x gl t t') or
   (match (kind_of_term t) with 
      | App (f,args) -> array_exists (fun t -> subterm gl t t') args
-     | Cast(t,_) -> (subterm gl t t')
+     | Cast(t,_,_) -> (subterm gl t t')
      | _ -> false)
            
 (*s We want to sort the list according to reverse subterm order. *)
@@ -386,7 +385,7 @@ let rec sort_subterm gl l =
   [gl: goal sigma]\\ *)
 
 let quote_terms ivs lc gl =
-  Library.check_required_library ["Coq";"ring";"Quote"];
+  Coqlib.check_required_library ["Coq";"ring";"Quote"];
   let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
   let varlist = ref ([] : constr list) in (* list of variables *)
   let counter = ref 1 in (* number of variables created + 1 *)
@@ -448,8 +447,8 @@ let quote f lid gl =
     | _ -> assert false
   in
   match ivs.variable_lhs with
-    | None -> Tactics.convert_concl (mkApp (f, [| p |])) gl
-    | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) gl
+    | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast gl
+    | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast gl
 
 (*i