diff options
| author |  puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-29 14:26:36 +0000 |
|---|---|---|
| committer | puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-29 14:26:36 +0000 |
| commit | 9752cb8aa72d4fa5921592f095032db756dcb229 (patch) | |
| tree | aa96836f442d481e241564061c9c42d73e2eb174 /plugins/firstorder/sequent.ml | |
| parent | a8299eca26974f287e0c14876dbaa947e0eaaf3c (diff) | |
Sequent: generic equality on constr replaced by destructors
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/firstorder/sequent.ml')
| -rw-r--r-- | plugins/firstorder/sequent.ml | 22 |
1 files changed, 21 insertions, 1 deletions
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 42d5a4ce5..85324e71a 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -113,7 +113,27 @@ let compare_constr_int f t1 t2 = | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> ((Pervasives.compare =? (compare_array f)) ==? (compare_array f)) ln1 ln2 tl1 tl2 bl1 bl2 - | _ -> Pervasives.compare t1 t2 + | Var _, (Rel _) + | Meta _, (Rel _ | Var _) + | Evar _, (Rel _ | Var _ | Meta _) + | Sort _, (Rel _ | Var _ | Meta _ | Evar _) + | Prod _, (Rel _ | Var _ | Meta _ | Evar _ | Sort _) + | Lambda _, (Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Prod _) + | LetIn _, (Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Prod _ | Lambda _) + | App _, (Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Prod _ | Lambda _ | LetIn _) + | Const _, (Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _) + | Ind _, (Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _ | Const _) + | Construct _, (Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _ | Const _ | Ind _) + | Case _, (Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _ | Const _ | Ind _ | Construct _) + | Fix _, (Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _ | Const _ | Ind _ | Construct _ | Case _) + | CoFix _, _ + -> -1 + | Rel _, _ | Var _, _ | Meta _, _ | Evar _, _ + | Sort _, _ | Prod _, _ + | Lambda _, _ | LetIn _, _ | App _, _ + | Const _, _ | Ind _, _ | Construct _, _ + | Case _, _| Fix _, _ + -> 1 let rec compare_constr m n= compare_constr_int compare_constr m n |