diff options
| author | pboutill | 2012-03-02 22:30:42 +0000 |
|---|---|---|
| committer | pboutill | 2012-03-02 22:30:42 +0000 |
| commit | c2dda7cf57f29e5746e5903c310a7ce88525909c (patch) | |
| tree | aa60a6f57014c20f980e90230b122cc76ba21e9b /pretyping/inductiveops.mli | |
| parent | 401f17afa2e9cc3f2d734aef0d71a2c363838ebd (diff) | |
"Let in" in pattern hell, one more iteration
This reverts commit 28bcf05dd876beea8697f6ee47ebf916a8b94cdf.
An other wrong externalize function
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15021 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 5cf84acd7a..3fb0907dfa 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -74,12 +74,20 @@ val inductive_nparams : inductive -> int val mis_constructor_nargs : constructor -> int val mis_constructor_nargs_env : env -> constructor -> int +(** @return param + args with letin *) +val mis_constructor_nhyps : constructor -> int +val mis_constructor_nhyps_env : env -> constructor -> int + (** @return args without letin *) val constructor_nrealargs : env -> constructor -> int (** @return args with letin *) val constructor_nrealhyps : constructor -> int +(** Is there local defs in params or args ? *) +val mis_constructor_has_local_defs : constructor -> bool +val inductive_has_local_defs : inductive -> bool + val get_full_arity_sign : env -> inductive -> rel_context val allowed_sorts : env -> inductive -> sorts_family list |