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 /plugins | |
| 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 'plugins')
| -rw-r--r-- | plugins/subtac/subtac_cases.ml | 16 |
1 files changed, 7 insertions, 9 deletions
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index d60841e72a..6893f13513 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -363,7 +363,7 @@ let unify_tomatch_with_patterns isevars env loc typ pats = let find_tomatch_tycon isevars env loc = function (* Try if some 'in I ...' is present and can be used as a constraint *) - | Some (_,ind,_,_) -> mk_tycon (inductive_template isevars env loc ind) + | Some (_,ind,_) -> mk_tycon (inductive_template isevars env loc ind) | None -> empty_tycon let coerce_row typing_fun isevars env pats (tomatch,(_,indopt)) = @@ -1414,7 +1414,7 @@ let extract_arity_signature env0 tomatchl tmsign = | NotInd (bo,typ) -> (match t with | None -> [na,Option.map (lift n) bo,lift n typ] - | Some (loc,_,_,_) -> + | Some (loc,_,_) -> user_err_loc (loc,"", str "Unexpected type annotation for a term of non inductive type")) | IsInd (_,IndType(indf,realargs)) -> @@ -1423,11 +1423,10 @@ let extract_arity_signature env0 tomatchl tmsign = let nrealargs = List.length realargs in let realnal = match t with - | Some (loc,ind',nparams,realnal) -> + | Some (loc,ind',realnal) -> if ind <> ind' then user_err_loc (loc,"",str "Wrong inductive type"); - if List.length params <> nparams - or nrealargs <> List.length realnal then + if nrealargs <> List.length realnal then anomaly "Ill-formed 'in' clause in cases"; List.rev realnal | None -> list_tabulate (fun _ -> Anonymous) nrealargs in @@ -1448,7 +1447,7 @@ let extract_arity_signatures env0 tomatchl tmsign = | NotInd (bo,typ) -> (match t with | None -> [na,bo,typ] - | Some (loc,_,_,_) -> + | Some (loc,_,_) -> user_err_loc (loc,"", str "Unexpected type annotation for a term of non inductive type")) | IsInd (_,IndType(indf,realargs)) -> @@ -1456,11 +1455,10 @@ let extract_arity_signatures env0 tomatchl tmsign = let nrealargs = List.length realargs in let realnal = match t with - | Some (loc,ind',nparams,realnal) -> + | Some (loc,ind',realnal) -> if ind <> ind' then user_err_loc (loc,"",str "Wrong inductive type"); - if List.length params <> nparams - or nrealargs <> List.length realnal then + if nrealargs <> List.length realnal then anomaly "Ill-formed 'in' clause in cases"; List.rev realnal | None -> list_tabulate (fun _ -> Anonymous) nrealargs in |