summaryrefslogtreecommitdiff
path: root/pretyping/classops.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
commit208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch)
tree591e9e512063e34099782e2518573f15ffeac003 /pretyping/classops.ml
parentde0085539583f59dc7c4bf4e272e18711d565466 (diff)
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'pretyping/classops.ml')
-rw-r--r--pretyping/classops.ml7
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index b6cce031..bbad005c 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: classops.ml 8642 2006-03-17 10:09:02Z notin $ *)
+(* $Id: classops.ml 9257 2006-10-21 17:28:28Z herbelin $ *)
open Util
open Pp
@@ -154,7 +154,8 @@ let lookup_pattern_path_between (s,t) =
coe.coe_value
in
match kind_of_term c with
- | Construct sp -> (sp, coe.coe_param)
+ | Construct cstr ->
+ (cstr, Inductiveops.constructor_nrealargs (Global.env()) cstr -1)
| _ -> raise Not_found) l
(* find_class_type : constr -> cl_typ * int *)
@@ -207,7 +208,7 @@ let class_of env sigma t =
let inductive_class_of ind = fst (class_info (CL_IND ind))
-let class_args_of c = snd (decompose_app c)
+let class_args_of c = snd (find_class_type c)
let string_of_class = function
| CL_FUN -> "Funclass"