diff options
| author | gregoire | 2005-12-02 10:01:15 +0000 |
|---|---|---|
| committer | gregoire | 2005-12-02 10:01:15 +0000 |
| commit | bf578ad5e2f63b7a36aeaef5e0597101db1bd24a (patch) | |
| tree | c0bc4e5f9ae67b8a03b28134dab3dcfe31d184dd /contrib/first-order | |
| parent | 825a338a1ddf1685d55bb5193aa5da078a534e1c (diff) | |
Changement des named_context
Ajout de cast indiquant au kernel la strategie a suivre
Resolution du bug sur les coinductifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/first-order')
| -rw-r--r-- | contrib/first-order/sequent.ml | 4 | ||||
| -rw-r--r-- | contrib/first-order/unify.ml | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml index 657d4cba52..fb75655f01 100644 --- a/contrib/first-order/sequent.ml +++ b/contrib/first-order/sequent.ml @@ -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 diff --git a/contrib/first-order/unify.ml b/contrib/first-order/unify.ml index a1e620a23d..41a100c2b1 100644 --- a/contrib/first-order/unify.ml +++ b/contrib/first-order/unify.ml @@ -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)-> |