diff options
| author | pboutill | 2012-03-02 22:30:44 +0000 |
|---|---|---|
| committer | pboutill | 2012-03-02 22:30:44 +0000 |
| commit | 0374e96684f9d3d38b1d54176a95281d47b21784 (patch) | |
| tree | f5598cd239e37c115a57a9dfd4be6630f94525e1 /interp/constrextern.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 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 57a025e32e..c08972ac15 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -727,7 +727,7 @@ let rec extern inctx scopes vars r = | Name id, GVar (_,id') when id=id' -> None | Name _, _ -> Some (dummy_loc,na) in (sub_extern false scopes vars tm, - (na',Option.map (fun (loc,ind,_,nal) -> + (na',Option.map (fun (loc,ind,nal) -> let args = List.map (fun x -> CPatAtom (dummy_loc, match x with Anonymous -> None | Name id -> Some (Ident (dummy_loc,id)))) nal in let full_args = add_patt_for_params ind args in let c = extern_reference loc vars (IndRef ind) in @@ -1011,8 +1011,8 @@ let rec glob_of_pat env = function in let indnames,rtn = match p, info.cip_ind, info.cip_ind_args with | PMeta None, _, _ -> (Anonymous,None),None - | _, Some ind, Some (nparams,nargs) -> - return_type_of_predicate ind nparams nargs (glob_of_pat env p) + | _, Some ind, Some nargs -> + return_type_of_predicate ind nargs (glob_of_pat env p) | _ -> anomaly "PCase with non-trivial predicate but unknown inductive" in GCases (loc,RegularStyle,rtn,[glob_of_pat env tm,indnames],mat) |