diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/glob_ops.ml | 10 | ||||
| -rw-r--r-- | pretyping/glob_ops.mli | 1 |
2 files changed, 9 insertions, 2 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 6b61b1452e..68626597fc 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -485,7 +485,11 @@ let is_gvar id c = match DAst.get c with | GVar id' -> Id.equal id id' | _ -> false -let rec cases_pattern_of_glob_constr na = DAst.map (function +let rec cases_pattern_of_glob_constr na c = + (* Forcing evaluation to ensure that the possible raising of + Not_found is not delayed *) + let c = DAst.force c in + DAst.map (function | GVar id -> begin match na with | Name _ -> @@ -498,6 +502,8 @@ let rec cases_pattern_of_glob_constr na = DAst.map (function | GApp (c, l) -> begin match DAst.get c with | GRef (ConstructRef cstr,_) -> + let nparams = Inductiveops.inductive_nparams (fst cstr) in + let _,l = List.chop nparams l in PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) | _ -> raise Not_found end @@ -505,7 +511,7 @@ let rec cases_pattern_of_glob_constr na = DAst.map (function (* A canonical encoding of aliases *) DAst.get (cases_pattern_of_glob_constr na' b) | _ -> raise Not_found - ) + ) c open Declarations open Term diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 91a2ef9c1e..c189a3bcb2 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -89,6 +89,7 @@ val map_pattern : (glob_constr -> glob_constr) -> (** Conversion from glob_constr to cases pattern, if possible + Evaluation is forced. Take the current alias as parameter, @raise Not_found if translation is impossible *) val cases_pattern_of_glob_constr : Name.t -> 'a glob_constr_g -> 'a cases_pattern_g |