diff options
| author | barras | 2001-05-23 15:13:07 +0000 |
|---|---|---|
| committer | barras | 2001-05-23 15:13:07 +0000 |
| commit | dc2e676c9cdedea43805c21a4b3203832a985f95 (patch) | |
| tree | 849760ef13d1460d603ce9436c244922e13a6080 /kernel/typeops.mli | |
| parent | a023ff2e48aaf7ebfb15e10dc7cdb80ab2991e8e (diff) | |
amelioration des messages d'erreurs vis a vis des evars
ajout automatique des chemins vers les sources au moment du Drop
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/typeops.mli')
| -rw-r--r-- | kernel/typeops.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 3008c87cb4..e4464fd899 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -39,7 +39,7 @@ val judge_of_prop_contents : contents -> unsafe_judgment val judge_of_type : universe -> unsafe_judgment * constraints (*s Type of atomic terms. *) -val relative : env -> 'a evar_map -> int -> unsafe_judgment +val relative : env -> int -> unsafe_judgment val type_of_constant : env -> 'a evar_map -> constant -> types @@ -85,11 +85,11 @@ val judge_of_case : env -> 'a evar_map -> case_info -> unsafe_judgment array -> unsafe_judgment * constraints val find_case_dep_nparams : - env -> 'a evar_map -> constr * constr -> inductive_family -> constr + env -> 'a evar_map -> constr * unsafe_judgment -> inductive_family -> bool * constraints val type_case_branches : - env -> 'a evar_map -> Inductive.inductive_type -> constr -> types + env -> 'a evar_map -> Inductive.inductive_type -> unsafe_judgment -> constr -> types array * types * constraints (*s Type of fixpoints and guard condition. *) |