diff options
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" |