diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-26 10:04:20 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-26 10:04:20 +0000 |
| commit | f572b02909b49533b58e14ef803316ccf9783dee (patch) | |
| tree | 26f5f0cd7395b105cbda87b2ad95efdf15ba3837 /toplevel/class.ml | |
| parent | 4b61463f5b95dad398a5e2ac444682793122af20 (diff) | |
Monomorphization (toplevel)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16005 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/class.ml')
| -rw-r--r-- | toplevel/class.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml index 87310302c..aa77a00c5 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -76,7 +76,7 @@ let check_arity = function (* check that the computed target is the provided one *) let check_target clt = function - | Some cl when cl <> clt -> raise (CoercionError (WrongTarget(clt,cl))) + | Some cl when not (cl_typ_eq cl clt) -> raise (CoercionError (WrongTarget(clt,cl))) | _ -> () (* condition d'heritage uniforme *) @@ -86,7 +86,7 @@ let uniform_cond nargs lt = | (0,[]) -> true | (n,t::l) -> let t = strip_outer_cast t in - isRel t && destRel t = n && aux ((n-1),l) + isRel t && Int.equal (destRel t) n && aux ((n-1),l) | _ -> false in aux (nargs,lt) @@ -127,7 +127,7 @@ let get_source lp source = | t1::lt -> try let cl1,lv1 = find_class_type Evd.empty t1 in - if cl = cl1 then cl1,lv1,(List.length lt+1) + if cl_typ_eq cl cl1 then cl1,lv1,(List.length lt+1) else raise Not_found with Not_found -> aux lt in aux (List.rev lp) |