diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
| commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
| tree | 591e9e512063e34099782e2518573f15ffeac003 /pretyping/classops.ml | |
| parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) | |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'pretyping/classops.ml')
| -rw-r--r-- | pretyping/classops.ml | 7 |
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" |