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

13 files changed, 77 insertions, 78 deletions

diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml
index 49cb8e25..fde48d2b 100644
--- a/contrib/first-order/formula.ml
+++ b/contrib/first-order/formula.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: formula.ml,v 1.18.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
+(* $Id: formula.ml 7493 2005-11-02 22:12:16Z mohring $ *)
 
 open Hipattern
 open Names
@@ -47,14 +47,14 @@ let rec nb_prod_after n c=
 
 let construct_nhyps ind gls =
   let env=pf_env gls in
-  let nparams = (snd (Global.lookup_inductive ind)).mind_nparams in
-  let constr_types = Inductive.arities_of_constructors (pf_env gls) ind in 
+  let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in
+  let constr_types = Inductiveops.arities_of_constructors (pf_env gls) ind in 
   let hyp = nb_prod_after nparams in	
     Array.map hyp constr_types
 
 (* indhyps builds the array of arrays of constructor hyps for (ind largs)*)
 let ind_hyps nevar ind largs gls= 
-  let types= Inductive.arities_of_constructors (pf_env gls) ind in 
+  let types= Inductiveops.arities_of_constructors (pf_env gls) ind in 
   let lp=Array.length types in     
   let myhyps i=
     let t1=Term.prod_applist types.(i) largs in
@@ -99,7 +99,7 @@ let rec kind_of_formula gl term =
 			let has_realargs=(n>0) in
 			let is_trivial=
 			  let is_constant c =
-			    nb_prod c = mip.mind_nparams in  
+			    nb_prod c = mib.mind_nparams in  
 			    array_exists is_constant mip.mind_nf_lc in 
 			  if Inductiveops.mis_is_recursive (ind,mib,mip) ||
 			    (has_realargs && not is_trivial)
diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli
index db24f20f..8703045c 100644
--- a/contrib/first-order/formula.mli
+++ b/contrib/first-order/formula.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: formula.mli,v 1.17.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
+(* $Id: formula.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Term
 open Names
diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4
index f85f2171..0970d5db 100644
--- a/contrib/first-order/g_ground.ml4
+++ b/contrib/first-order/g_ground.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma"  i*)
 
-(* $Id: g_ground.ml4,v 1.10.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
+(* $Id: g_ground.ml4 7909 2006-01-21 11:09:18Z herbelin $ *)
 
 open Formula
 open Sequent
@@ -41,7 +41,7 @@ let _=
       
 let default_solver=(Tacinterp.interp <:tactic<auto with *>>)
     
-let fail_solver=tclFAIL 0 "GTauto failed"
+let fail_solver=tclFAIL 0 (Pp.str "GTauto failed")
 		      
 type external_env=
     Ids of global_reference list
@@ -81,23 +81,16 @@ let normalize_evaluables=
 	   unfold_in_hyp (Lazy.force defined_connectives) 
 	   (Tacexpr.InHypType id)) *)
 
-TACTIC EXTEND Firstorder
-    [ "Firstorder" tactic_opt(t) "with" ne_reference_list(l) ] -> 
+TACTIC EXTEND firstorder
+    [ "firstorder" tactic_opt(t) "with" ne_reference_list(l) ] -> 
       [ gen_ground_tac true (option_app eval_tactic t) (Ids l) ]
-|   [ "Firstorder" tactic_opt(t) "using" ne_preident_list(l) ] -> 
+|   [ "firstorder" tactic_opt(t) "using" ne_preident_list(l) ] -> 
       [ gen_ground_tac true (option_app eval_tactic t) (Bases l) ]
-|   [ "Firstorder" tactic_opt(t) ] -> 
+|   [ "firstorder" tactic_opt(t) ] -> 
       [ gen_ground_tac true (option_app eval_tactic t) Void ]
 END
 
-(* Obsolete since V8.0
-TACTIC EXTEND GTauto   
-  [ "GTauto" ] ->
-     [ gen_ground_tac false (Some fail_solver) Void ]   
-END
-*)
-
-TACTIC EXTEND GIntuition
-  [ "GIntuition" tactic_opt(t) ] ->
+TACTIC EXTEND gintuition
+  [ "gintuition" tactic_opt(t) ] ->
      [ gen_ground_tac false (option_app eval_tactic t) Void ]
 END
diff --git a/contrib/first-order/ground.ml b/contrib/first-order/ground.ml
index 23e27a3c..bb096308 100644
--- a/contrib/first-order/ground.ml
+++ b/contrib/first-order/ground.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ground.ml,v 1.5.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
+(* $Id: ground.ml 7909 2006-01-21 11:09:18Z herbelin $ *)
 
 open Formula
 open Sequent
@@ -45,23 +45,23 @@ let update_flags ()=
 *)
 
 let update_flags ()=
-  let predref=ref Names.KNpred.empty in
+  let predref=ref Names.Cpred.empty in
   let f coe=
     try
       let kn=destConst (Classops.get_coercion_value coe) in
-	predref:=Names.KNpred.add kn !predref
+	predref:=Names.Cpred.add kn !predref
     with Invalid_argument "destConst"-> () in
     List.iter f (Classops.coercions ());
     red_flags:=
     Closure.RedFlags.red_add_transparent 
       Closure.betaiotazeta 
-      (Names.Idpred.full,Names.KNpred.complement !predref)
+      (Names.Idpred.full,Names.Cpred.complement !predref)
 
 let ground_tac solver startseq gl=
   update_flags ();
   let rec toptac skipped seq gl=
     if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
-    then Pp.msgnl (Proof_trees.pr_goal (sig_it gl));
+    then Pp.msgnl (Printer.pr_goal (sig_it gl));
     tclORELSE (axiom_tac seq.gl seq)
       begin
 	try      
@@ -78,7 +78,7 @@ let ground_tac solver startseq gl=
 		      | Rforall->
 			  let backtrack1=
 			    if !qflag then 
-			      tclFAIL 0 "reversible in 1st order mode"
+			      tclFAIL 0 (Pp.str "reversible in 1st order mode")
 			    else
 			      backtrack in
 			    forall_tac backtrack continue (re_add seq1)
@@ -117,7 +117,8 @@ let ground_tac solver startseq gl=
 			      backtrack2 (* need special backtracking *)
   		      | Lexists ind ->
 			  if !qflag then 
-			    left_exists_tac ind hd.id continue (re_add seq1)
+			    left_exists_tac ind backtrack hd.id
+			      continue (re_add seq1)
 			  else backtrack
 		      | LA (typ,lap)->
 			  let la_tac=
diff --git a/contrib/first-order/ground.mli b/contrib/first-order/ground.mli
index cfc17e77..621f99db 100644
--- a/contrib/first-order/ground.mli
+++ b/contrib/first-order/ground.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ground.mli,v 1.1.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
+(* $Id: ground.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 val ground_tac:     Tacmach.tactic ->
   (Proof_type.goal Tacmach.sigma -> Sequent.t) -> Tacmach.tactic
diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml
index e2e9e2ef..254d7b84 100644
--- a/contrib/first-order/instances.ml
+++ b/contrib/first-order/instances.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: instances.ml,v 1.9.2.1 2004/07/16 19:30:10 herbelin Exp $ i*)
+(*i $Id: instances.ml 8654 2006-03-22 15:36:58Z msozeau $ i*)
 
 open Formula
 open Sequent
@@ -105,10 +105,10 @@ let dummy_bvid=id_of_string "x"
 
 let mk_open_instance id gl m t=
   let env=pf_env gl in
-  let evmap=Refiner.sig_sig gl in
+  let evmap=Refiner.project gl in
   let var_id=
     if id==dummy_id then dummy_bvid else
-      let typ=pf_type_of gl (constr_of_reference id) in
+      let typ=pf_type_of gl (constr_of_global id) in
 	(* since we know we will get a product, 
 	   reduction is not too expensive *)
       let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in
@@ -121,15 +121,18 @@ let mk_open_instance id gl m t=
       let nid=(fresh_id avoid var_id gl) in
 	(Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in
   let nt=it_mkLambda_or_LetIn revt (aux m []) in
-  let rawt=Detyping.detype (false,env) [] [] nt in
+  let rawt=Detyping.detype false [] [] nt in
   let rec raux n t=
     if n=0 then t else 
       match t with
 	  RLambda(loc,name,_,t0)->
 	    let t1=raux (n-1) t0 in
-	      RLambda(loc,name,RHole (dummy_loc,BinderType name),t1)
+	      RLambda(loc,name,RHole (dummy_loc,Evd.BinderType name),t1)
 	| _-> anomaly "can't happen" in
-  let ntt=Pretyping.understand evmap env (raux m rawt) in
+  let ntt=try 
+    Pretyping.Default.understand evmap env (raux m rawt)
+  with _ -> 
+    error "Untypable instance, maybe higher-order non-prenex quantification" in
     Sign.decompose_lam_n_assum m ntt
 
 (* tactics   *)
@@ -138,13 +141,13 @@ let left_instance_tac (inst,id) continue seq=
   match inst with
       Phantom dom->
 	if lookup (id,None) seq then 
-	  tclFAIL 0 "already done"
+	  tclFAIL 0 (Pp.str "already done")
 	else
 	  tclTHENS (cut dom) 
 	    [tclTHENLIST
 	       [introf;
 		(fun gls->generalize 
-		   [mkApp(constr_of_reference id,
+		   [mkApp(constr_of_global id,
 			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
 		introf;
 		tclSOLVE [wrap 1 false continue 
@@ -152,7 +155,7 @@ let left_instance_tac (inst,id) continue seq=
 	    tclTRY assumption]
     | Real((m,t) as c,_)->
 	if lookup (id,Some c) seq then 
-	  tclFAIL 0 "already done" 
+	  tclFAIL 0 (Pp.str "already done")
 	else 
 	  let special_generalize=
 	    if m>0 then 
@@ -160,10 +163,10 @@ let left_instance_tac (inst,id) continue seq=
 		let (rc,ot)= mk_open_instance id gl m t in
 		let gt= 
 		  it_mkLambda_or_LetIn 
-		    (mkApp(constr_of_reference id,[|ot|])) rc in
+		    (mkApp(constr_of_global id,[|ot|])) rc in
 		  generalize [gt] gl
 	    else
-	      generalize [mkApp(constr_of_reference id,[|t|])]
+	      generalize [mkApp(constr_of_global id,[|t|])]
 	  in
 	    tclTHENLIST 
 	      [special_generalize;
@@ -186,7 +189,7 @@ let right_instance_tac inst continue seq=
 	(tclTHEN (split (Rawterm.ImplicitBindings [t]))
 	   (tclSOLVE [wrap 0 true continue (deepen seq)]))
     | Real ((m,t),_) ->
-	tclFAIL 0 "not implemented ... yet"
+	tclFAIL 0 (Pp.str "not implemented ... yet")
 
 let instance_tac inst=
   if (snd inst)==dummy_id then 
diff --git a/contrib/first-order/instances.mli b/contrib/first-order/instances.mli
index 509bfc70..7667c89f 100644
--- a/contrib/first-order/instances.mli
+++ b/contrib/first-order/instances.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: instances.mli,v 1.3.2.1 2004/07/16 19:30:10 herbelin Exp $ i*)
+(*i $Id: instances.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 open Term
 open Tacmach
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index 7fbefa37..f6653b82 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: rules.ml,v 1.24.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
+(* $Id: rules.ml 7909 2006-01-21 11:09:18Z herbelin $ *)
 
 open Util
 open Names
@@ -57,18 +57,18 @@ let clear_global=function
 (* connection rules *)
 
 let axiom_tac t seq=
-  try exact_no_check (constr_of_reference (find_left t seq)) 
-  with Not_found->tclFAIL 0 "No axiom link" 
+  try exact_no_check (constr_of_global (find_left t seq)) 
+  with Not_found->tclFAIL 0 (Pp.str "No axiom link")
 
 let ll_atom_tac a backtrack id continue seq= 
   tclIFTHENELSE
     (try 
       tclTHENLIST
-	[generalize [mkApp(constr_of_reference id,
-			   [|constr_of_reference (find_left a seq)|])];
+	[generalize [mkApp(constr_of_global id,
+			   [|constr_of_global (find_left a seq)|])];
 	 clear_global id;
 	 intro]
-    with Not_found->tclFAIL 0 "No link") 
+    with Not_found->tclFAIL 0 (Pp.str "No link"))
     (wrap 1 false continue seq) backtrack 
 
 (* right connectives rules *)
@@ -92,7 +92,7 @@ let left_and_tac ind backtrack id continue seq gls=
  let n=(construct_nhyps ind gls).(0) in  
    tclIFTHENELSE
      (tclTHENLIST 
-      [simplest_elim (constr_of_reference id);
+      [simplest_elim (constr_of_global id);
        clear_global id; 
        tclDO n intro])
      (wrap n false continue seq)
@@ -106,12 +106,12 @@ let left_or_tac ind backtrack id continue seq gls=
        tclDO n intro;
        wrap n false continue seq] in
     tclIFTHENSVELSE
-      (simplest_elim (constr_of_reference id))
+      (simplest_elim (constr_of_global id))
       (Array.map f v)
       backtrack gls
 
 let left_false_tac id=
-  simplest_elim (constr_of_reference id)
+  simplest_elim (constr_of_global id)
 
 (* left arrow connective rules *)
 
@@ -127,7 +127,7 @@ let ll_ind_tac ind largs backtrack id continue seq gl=
        let cstr=mkApp ((mkConstruct (ind,(i+1))),vargs) in
        let vars=Array.init p (fun j->mkRel (p-j)) in
        let capply=mkApp ((lift p cstr),vars) in
-       let head=mkApp ((lift p (constr_of_reference id)),[|capply|]) in
+       let head=mkApp ((lift p (constr_of_global id)),[|capply|]) in
 	 Sign.it_mkLambda_or_LetIn head rc in
        let lp=Array.length rcs in
        let newhyps=list_tabulate myterm lp in
@@ -141,7 +141,7 @@ let ll_ind_tac ind largs backtrack id continue seq gl=
 let ll_arrow_tac a b c backtrack id continue seq=
   let cc=mkProd(Anonymous,a,(lift 1 b)) in
   let d=mkLambda (Anonymous,b,
-		  mkApp ((constr_of_reference id),
+		  mkApp ((constr_of_global id),
 			 [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
     tclORELSE
       (tclTHENS (cut c)
@@ -150,7 +150,7 @@ let ll_arrow_tac a b c backtrack id continue seq=
 	     clear_global id;
 	     wrap 1 false continue seq];
 	  tclTHENS (cut cc) 
-            [exact_no_check (constr_of_reference id); 
+            [exact_no_check (constr_of_global id); 
 	     tclTHENLIST 
 	       [generalize [d];
 		clear_global id;
@@ -168,17 +168,19 @@ let forall_tac backtrack continue seq=
 	  (tclTHEN introf (tclCOMPLETE (wrap 0 true continue seq)))
 	  backtrack))
     (if !qflag then 
-       tclFAIL 0 "reversible in 1st order mode"
+       tclFAIL 0 (Pp.str "reversible in 1st order mode")
      else
        backtrack)
 
-let left_exists_tac ind id continue seq gls=
+let left_exists_tac ind backtrack id continue seq gls=
   let n=(construct_nhyps ind gls).(0) in  
-    tclTHENLIST
-      [simplest_elim (constr_of_reference id);
-       clear_global id;
-       tclDO n intro;
-       (wrap (n-1) false continue seq)] gls
+    tclIFTHENELSE
+      (simplest_elim (constr_of_global id))
+      (tclTHENLIST [clear_global id;
+                    tclDO n intro;
+                    (wrap (n-1) false continue seq)]) 
+      backtrack 
+      gls
 	
 let ll_forall_tac prod backtrack id continue seq=
   tclORELSE
@@ -187,7 +189,7 @@ let ll_forall_tac prod backtrack id continue seq=
 	  [intro;
 	   (fun gls->
 	      let id0=pf_nth_hyp_id gls 1 in
-	      let term=mkApp((constr_of_reference id),[|mkVar(id0)|]) in
+	      let term=mkApp((constr_of_global id),[|mkVar(id0)|]) in
 		tclTHEN (generalize [term]) (clear [id0]) gls);  
 	   clear_global id;
 	   intro;
@@ -211,4 +213,4 @@ let normalize_evaluables=
 	 None->unfold_in_concl (Lazy.force defined_connectives)
        | Some (id,_,_)-> 
 	   unfold_in_hyp (Lazy.force defined_connectives) 
-	   (id,[],(Tacexpr.InHypTypeOnly,ref None)))
+	   (id,[],Tacexpr.InHypTypeOnly))
diff --git a/contrib/first-order/rules.mli b/contrib/first-order/rules.mli
index eb4d81bd..3798d8d4 100644
--- a/contrib/first-order/rules.mli
+++ b/contrib/first-order/rules.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: rules.mli,v 1.11.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
+(* $Id: rules.mli 6141 2004-09-27 14:55:34Z corbinea $ *)
 
 open Term
 open Tacmach
@@ -47,7 +47,7 @@ val ll_arrow_tac : constr -> constr -> constr -> lseqtac with_backtracking
 
 val forall_tac : seqtac with_backtracking
 
-val left_exists_tac : inductive -> lseqtac
+val left_exists_tac : inductive -> lseqtac with_backtracking
 
 val ll_forall_tac : types -> lseqtac with_backtracking 
 
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
index 13215348..805700b0 100644
--- a/contrib/first-order/sequent.ml
+++ b/contrib/first-order/sequent.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: sequent.ml,v 1.17.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
+(* $Id: sequent.ml 7925 2006-01-24 23:20:39Z herbelin $ *)
 
 open Term
 open Util
@@ -91,8 +91,8 @@ let compare_constr_int f t1 t2 =
     | Meta m1, Meta m2 -> m1 - m2
     | Var id1, Var id2 -> Pervasives.compare id1 id2
     | Sort s1, Sort s2 -> Pervasives.compare s1 s2
-    | Cast (c1,_), _ -> f c1 t2
-    | _, Cast (c2,_) -> f t1 c2
+    | Cast (c1,_,_), _ -> f c1 t2
+    | _, Cast (c2,_,_) -> f t1 c2
     | Prod (_,t1,c1), Prod (_,t2,c2) 
     | Lambda (_,t1,c1), Lambda (_,t2,c2) ->
 	(f =? f) t1 t2 c1 c2 
@@ -255,7 +255,7 @@ let empty_seq depth=
 
 let create_with_ref_list l depth gl=
   let f gr seq=
-    let c=constr_of_reference gr in    
+    let c=constr_of_global gr in    
     let typ=(pf_type_of gl c) in
       add_formula Hyp gr typ seq gl in
     List.fold_right f l (empty_seq depth)
@@ -269,7 +269,7 @@ let create_with_auto_hints l depth gl=
 	Res_pf (c,_) | Give_exact c
       | Res_pf_THEN_trivial_fail (c,_) ->
 	  (try 
-	     let gr=reference_of_constr c in 
+	     let gr=global_of_constr c in 
 	     let typ=(pf_type_of gl c) in
 	       seqref:=add_formula Hint gr typ !seqref gl
 	   with Not_found->())
@@ -278,7 +278,7 @@ let create_with_auto_hints l depth gl=
   let h dbname=
     let hdb=
       try
-	Util.Stringmap.find dbname !searchtable 
+	searchtable_map dbname
       with Not_found-> 
 	error ("Firstorder: "^dbname^" : No such Hint database") in
       Hint_db.iter g hdb in
@@ -289,9 +289,9 @@ let print_cmap map=
   let print_entry c l s=
     let xc=Constrextern.extern_constr false (Global.env ()) c in
       str "| " ++ 
-      Util.prlist (Ppconstr.pr_global Idset.empty) l ++ 
+      Util.prlist Printer.pr_global l ++ 
       str " : " ++
-      Ppconstr.pr_constr xc ++ 
+      Ppconstr.pr_constr_expr xc ++ 
       cut () ++ 
       s in
     msgnl (v 0 
diff --git a/contrib/first-order/sequent.mli b/contrib/first-order/sequent.mli
index df27d2ff..47fb74c7 100644
--- a/contrib/first-order/sequent.mli
+++ b/contrib/first-order/sequent.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: sequent.mli,v 1.8.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
+(* $Id: sequent.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Term
 open Util
diff --git a/contrib/first-order/unify.ml b/contrib/first-order/unify.ml
index 1186fb90..1dd13cbe 100644
--- a/contrib/first-order/unify.ml
+++ b/contrib/first-order/unify.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: unify.ml,v 1.10.2.1 2004/07/16 19:30:10 herbelin Exp $ i*)
+(*i $Id: unify.ml 7639 2005-12-02 10:01:15Z gregoire $ i*)
 
 open Util
 open Formula 
@@ -59,8 +59,8 @@ let unif t1 t2=
 		if Intset.is_empty (free_rels t) && 
 		  not (occur_term (mkMeta i) t) then
 		    bind i t else raise (UFAIL(nt1,nt2))
-	  | Cast(_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige
- 	  | _,Cast(_,_)->Queue.add (nt1,strip_outer_cast nt2) bige 
+	  | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige
+ 	  | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige 
 	  | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))->
 	      Queue.add (a,c) bige;Queue.add (pop b,pop d) bige
 	  | Case (_,pa,ca,va),Case (_,pb,cb,vb)->
diff --git a/contrib/first-order/unify.mli b/contrib/first-order/unify.mli
index dd9dbdec..9fbe3dda 100644
--- a/contrib/first-order/unify.mli
+++ b/contrib/first-order/unify.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: unify.mli,v 1.7.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
+(* $Id: unify.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Term