Traduction constr->rawconstr (avant dans Termast

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@271 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 27 insertions, 0 deletions

diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
new file mode 100644
index 0000000000..8f51823f49
--- /dev/null
+++ b/pretyping/detyping.mli
@@ -0,0 +1,27 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Term
+open Sign
+open Rawterm
+(*i*)
+
+(* [detype avoid env c] turns [c], typed in [env], into a rawconstr. *)
+(* De Bruijn indexes are turned to bound names, avoiding names in [avoid] *)
+
+exception StillDLAM
+
+val detype : identifier list -> unit assumptions -> constr -> rawconstr
+
+(* look for the index of a named var or a nondep var as it is renamed *)
+val lookup_name_as_renamed :
+  unit assumptions -> constr -> identifier -> int option
+val lookup_index_as_renamed : constr -> int -> int option
+
+
+val force_wildcard : unit -> bool
+val synthetize_type : unit -> bool
+val force_if : inductive_path -> bool
+val force_let : inductive_path -> bool