Ground update

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

4 files changed, 27 insertions, 8 deletions

diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml
index 8625c988d3..e38af4c0c9 100644
--- a/contrib/first-order/instances.ml
+++ b/contrib/first-order/instances.ml
@@ -27,10 +27,6 @@ open Libnames
 let rev_rels n t= (* requires n = max (free_rels t) *) 
   let l=list_tabulate (fun i->mkRel (n-i)) n in
     substl l t
- 	  
-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
 
 (* ordre lexico:
    nombre de metas dans terme;
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
index 91a8f1ddd8..c63c10f43a 100644
--- a/contrib/first-order/sequent.ml
+++ b/contrib/first-order/sequent.ml
@@ -169,7 +169,16 @@ let deepen seq={seq with depth=seq.depth-1}
  
 let record item seq={seq with history=History.add item seq.history}
 
-let lookup item seq=History.mem item seq.history
+let lookup item seq=
+  History.mem item seq.history ||
+  match item with
+      (_,None)->false
+    | (id,Some ((m,t) as c))->
+	let p (id2,o)=
+	  match o with
+	      None -> false
+	    | Some ((m2,t2) as c2)->id=id2 && m2>m && more_general c2 c in
+	  History.exists p seq.history
 
 let add_left (nam,t) seq internal gl=
   match build_left_entry nam t internal gl seq.cnt with
diff --git a/contrib/first-order/unify.ml b/contrib/first-order/unify.ml
index 30ff1c811d..ffe0070409 100644
--- a/contrib/first-order/unify.ml
+++ b/contrib/first-order/unify.ml
@@ -102,8 +102,8 @@ let value i t=
     vaux t
 	  
 type instance=
-    Real of (int*constr)*int (* nb trous*terme*valeur heuristique *)
-  | Phantom of constr (* domaine de quantification *)
+    Real of (int*constr)*int 
+  | Phantom of constr 
 
 let mk_rel_inst t=
   let new_rel=ref 1 in
@@ -131,4 +131,16 @@ let unif_atoms i dom t1 t2=
     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 || is_head_meta t in
+	List.for_all p sigma
+    with UFAIL(_,_)->false
diff --git a/contrib/first-order/unify.mli b/contrib/first-order/unify.mli
index 013fc73cd1..7e00819517 100644
--- a/contrib/first-order/unify.mli
+++ b/contrib/first-order/unify.mli
@@ -19,3 +19,5 @@ type instance=
   | Phantom of constr        (* domaine de quantification *)
 
 val unif_atoms : metavariable -> constr -> constr -> constr -> instance option
+
+val more_general : (int*constr) -> (int*constr) -> bool