diff options
Diffstat (limited to 'pretyping/detyping.mli')
| -rw-r--r-- | pretyping/detyping.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 7ac7162f..23090858 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: detyping.mli 9976 2007-07-12 11:58:30Z msozeau $ i*) +(*i $Id: detyping.mli 10410 2007-12-31 13:11:55Z msozeau $ i*) (*i*) open Util @@ -40,6 +40,9 @@ val detype_case : val detype_sort : sorts -> rawsort +val detype_rel_context : constr option -> identifier list -> names_context -> + rel_context -> rawdecl list + (* look for the index of a named var or a nondep var as it is renamed *) val lookup_name_as_renamed : env -> constr -> identifier -> int option val lookup_index_as_renamed : env -> constr -> int -> int option @@ -47,8 +50,6 @@ val lookup_index_as_renamed : env -> constr -> int -> int option val set_detype_anonymous : (loc -> int -> rawconstr) -> unit val force_wildcard : unit -> bool val synthetize_type : unit -> bool -val force_if : case_info -> bool -val force_let : case_info -> bool (* Utilities to transform kernel cases to simple pattern-matching problem *) @@ -57,4 +58,3 @@ val simple_cases_matrix_of_branches : inductive -> int list -> rawconstr list -> cases_clauses val return_type_of_predicate : inductive -> int -> int -> rawconstr -> predicate_pattern * rawconstr option - |