diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 40d0465741..ff494c7825 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -899,7 +899,7 @@ let rec raw_of_pat env = function let k = mip.Declarations.mind_nrealargs in let nparams = mib.Declarations.mind_nparams in let cstrnargs = mip.Declarations.mind_consnrealargs in - Detyping.detype_case false (raw_of_pat env)(raw_of_eqn env) + Detyping.detype_case false (raw_of_pat env) (raw_of_eqns env) (fun _ _ -> false (* lazy: don't try to display pattern with "if" *)) avoid (ind,cs,nparams,cstrnargs,k) typopt tm bv | PCase _ -> error "Unsupported case-analysis while printing pattern" @@ -907,6 +907,9 @@ let rec raw_of_pat env = function | PCoFix c -> Detyping.detype false [] env (mkCoFix c) | PSort s -> RSort (loc,s) +and raw_of_eqns env constructs consnargsl bl = + Array.to_list (array_map3 (raw_of_eqn env) constructs consnargsl bl) + and raw_of_eqn env constr construct_nargs branch = let make_pat x env b ids = let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in |