diff options
| author | herbelin | 2006-01-16 14:03:05 +0000 |
|---|---|---|
| committer | herbelin | 2006-01-16 14:03:05 +0000 |
| commit | 655f6a6305812d3f95d27f5579e119523ae3bef0 (patch) | |
| tree | 0bc3e45faeea4fe18c388aa69e2722dc600b1e2a /interp | |
| parent | 58529cf2252bf6ae386a45c8587bdc9b3285c1c5 (diff) | |
Version préliminaire d'inversion de la compilation du filtrage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7881 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |