Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 0 insertions, 143 deletions

diff --git a/contrib/firstorder/unify.ml b/contrib/firstorder/unify.ml
deleted file mode 100644
index 27c06f54..00000000
--- a/contrib/firstorder/unify.ml
+++ /dev/null
@@ -1,143 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: unify.ml 11897 2009-02-09 19:28:02Z barras $ i*)
-
-open Util
-open Formula 
-open Tacmach
-open Term
-open Names
-open Termops
-open Reductionops
-
-exception UFAIL of constr*constr
-
-(* 
-   RIGID-only Martelli-Montanari style unification for CLOSED terms 
-   I repeat : t1 and t2 must NOT have ANY free deBruijn                        
-   sigma is kept normal with respect to itself but is lazily applied 
-   to the equation set. Raises UFAIL with a pair of  terms 
-*)
-
-let unif t1 t2= 
-  let bige=Queue.create () 
-  and sigma=ref [] in
-  let bind i t=
-    sigma:=(i,t)::
-      (List.map (function (n,tn)->(n,subst_meta [i,t] tn)) !sigma) in
-  let rec head_reduce t= 
-    (* forbids non-sigma-normal meta in head position*)
-    match kind_of_term t with
-	Meta i->
-	  (try 
-	     head_reduce (List.assoc i !sigma) 
-	   with Not_found->t)
-      | _->t in 
-    Queue.add (t1,t2) bige;
-    try while true do
-      let t1,t2=Queue.take bige in
-      let nt1=head_reduce (whd_betaiotazeta Evd.empty t1) 
-      and nt2=head_reduce (whd_betaiotazeta Evd.empty t2) in
-	match (kind_of_term nt1),(kind_of_term nt2) with
-	    Meta i,Meta j-> 
-	      if i<>j then 
-		if i<j then bind j nt1
-		else bind i nt2
-	  | Meta i,_ ->
-	      let t=subst_meta !sigma nt2 in
-		if Intset.is_empty (free_rels t) && 
-		  not (occur_term (mkMeta i) t) then
-		    bind i t else raise (UFAIL(nt1,nt2))
-	  | _,Meta i -> 
-	      let t=subst_meta !sigma nt1 in
-		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 
-	  | (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)->
-	      Queue.add (pa,pb) bige;
-	      Queue.add (ca,cb) bige;
-	      let l=Array.length va in
-		if l<>(Array.length vb) then 
-		  raise (UFAIL (nt1,nt2))
-		else 
-		  for i=0 to l-1 do
-		    Queue.add (va.(i),vb.(i)) bige
-		  done	  
-	  | App(ha,va),App(hb,vb)->
-	      Queue.add (ha,hb) bige;
-	      let l=Array.length va in
-		if l<>(Array.length vb) then 
-		  raise (UFAIL (nt1,nt2))
-		else 
-		  for i=0 to l-1 do
-		    Queue.add (va.(i),vb.(i)) bige
-		  done
-	  | _->if not (eq_constr nt1 nt2) then raise (UFAIL (nt1,nt2))
-    done;
-      assert false 
-	(* this place is unreachable but needed for the sake of typing *)
-    with Queue.Empty-> !sigma
-
-let value i t=
-  let add x y=
-    if x<0 then y else if y<0 then x else x+y in
-  let tref=mkMeta i in
-  let rec vaux term=
-    if term=tref then 0 else 
-      let f v t=add v (vaux t) in
-      let vr=fold_constr f (-1) term in
-	if vr<0 then -1 else vr+1 in
-    vaux t
-	  
-type instance=
-    Real of (int*constr)*int 
-  | Phantom of constr 
-
-let mk_rel_inst t=
-  let new_rel=ref 1 in
-  let rel_env=ref [] in
-  let rec renum_rec d t=
-    match kind_of_term t with 
-	Meta n->
-	  (try 
-	     mkRel (d+(List.assoc n !rel_env))
-	   with Not_found->
-	     let m= !new_rel in
-	       incr new_rel;
-	       rel_env:=(n,m) :: !rel_env;
-	       mkRel (m+d))
-      | _ -> map_constr_with_binders succ renum_rec d t
-  in 
-  let nt=renum_rec 0 t in (!new_rel - 1,nt)
-
-let unif_atoms i dom t1 t2=
-  try 
-    let t=List.assoc i (unif t1 t2) in 
-      if isMeta t then Some (Phantom dom)
-      else Some (Real(mk_rel_inst t,value i t1))
-  with
-      UFAIL(_,_) ->None
-    | Not_found ->Some (Phantom dom)
-	   	  
-let renum_metas_from k n t= (* requires n = max (free_rels t) *)
-  let l=list_tabulate (fun i->mkMeta (k+i)) n in
-    substl l t
-
-let more_general (m1,t1) (m2,t2)=
-  let mt1=renum_metas_from 0 m1 t1
-  and mt2=renum_metas_from m1 m2 t2 in
-    try 
-      let sigma=unif mt1 mt2 in
-      let p (n,t)= n<m1 || isMeta t in
-	List.for_all p sigma
-    with UFAIL(_,_)->false