diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-02 22:30:44 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-02 22:30:44 +0000 |
| commit | 0374e96684f9d3d38b1d54176a95281d47b21784 (patch) | |
| tree | f5598cd239e37c115a57a9dfd4be6630f94525e1 /pretyping/pattern.ml | |
| parent | c2dda7cf57f29e5746e5903c310a7ce88525909c (diff) | |
Glob_term.predicate_pattern: No number of parameters with letins.
Detyping is wrong about it and as far as I understand no one but Constrextern uses
it. Constrextern has now the same machinery for all patterns.
Revert if I miss something.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15022 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pattern.ml')
| -rw-r--r-- | pretyping/pattern.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 49b63a4b5..0610c00f1 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -30,7 +30,7 @@ type extended_patvar_map = (patvar * constr_under_binders) list type case_info_pattern = { cip_style : case_style; cip_ind : inductive option; - cip_ind_args : (int * int) option; (** number of params and args *) + cip_ind_args : int option; (** number of args *) cip_extensible : bool (** does this match end with _ => _ ? *) } type constr_pattern = @@ -133,7 +133,7 @@ let pattern_of_constr sigma t = let cip = { cip_style = ci.ci_pp_info.style; cip_ind = Some ci.ci_ind; - cip_ind_args = Some (ci.ci_npar, ci.ci_pp_info.ind_nargs); + cip_ind_args = Some (ci.ci_pp_info.ind_nargs); cip_extensible = false } in let branch_of_constr i c = @@ -324,13 +324,13 @@ let rec pat_of_raw metas vars = function | _ -> None in let ind_nargs,ind = match indnames with - | Some (_,ind,n,nal) -> Some (n,List.length nal), Some ind + | Some (_,ind,nal) -> Some (List.length nal), Some ind | None -> None, get_ind brs in let ext,brs = pats_of_glob_branches loc metas vars ind brs in let pred = match p,indnames with - | Some p, Some (_,_,_,nal) -> + | Some p, Some (_,_,nal) -> rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas vars p)) | _ -> PMeta None in |