diff options
author | 1999-10-13 13:33:28 +0000 | |
---|---|---|
committer | 1999-10-13 13:33:28 +0000 | |
commit | 62ae7054f871b77207fab5c2fab1fbcd7e5124a9 (patch) | |
tree | 83f61e40a292149e45dc11cee8e1db20a67691b4 | |
parent | f39e92e127d551c4d9413de9c660afce5275c341 (diff) |
organisation de trad (entre parsing/ et pretyping/)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@102 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | parsing/astterm.mli | 24 | ||||
-rw-r--r-- | parsing/printer.mli | 17 | ||||
-rw-r--r-- | parsing/termast.mli | 17 | ||||
-rw-r--r-- | pretyping/class.mli | 2 | ||||
-rw-r--r-- | pretyping/evarconv.mli | 2 | ||||
-rw-r--r-- | pretyping/evarutil.mli | 2 | ||||
-rw-r--r-- | pretyping/multcase.mli | 2 | ||||
-rw-r--r-- | pretyping/pretyping.mli | 2 | ||||
-rw-r--r-- | pretyping/record.mli | 2 |
9 files changed, 70 insertions, 0 deletions
diff --git a/parsing/astterm.mli b/parsing/astterm.mli new file mode 100644 index 000000000..0f3113bf6 --- /dev/null +++ b/parsing/astterm.mli @@ -0,0 +1,24 @@ + +(* $Id$ *) + +(*i*) +open Names +open Term +open Environ +(*i*) + +val dbize_op : + Coqast.loc -> string -> Coqast.t list -> pseudo_constr list -> pseudo_constr +val dbize : unit assumptions -> Coqast.t -> pseudo_constr + +val absolutize_cci : unsafe_env -> pseudo_constr -> pseudo_constr +val dbize_cci : unsafe_env -> Coqast.t -> pseudo_constr +val absolutize_fw : unsafe_env -> pseudo_constr -> pseudo_constr +val dbize_fw : unsafe_env -> Coqast.t -> pseudo_constr + +val raw_pseudo_constr_of_com : unsafe_env -> Coqast.t -> pseudo_constr +val raw_fpseudo_constr_of_com : unsafe_env -> Coqast.t -> pseudo_constr +val raw_pseudo_constr_of_compattern : unsafe_env -> Coqast.t -> pseudo_constr + +val globalize_command : Coqast.t -> Coqast.t +val globalize_ast : Coqast.t -> Coqast.t diff --git a/parsing/printer.mli b/parsing/printer.mli new file mode 100644 index 000000000..bcdc6f93a --- /dev/null +++ b/parsing/printer.mli @@ -0,0 +1,17 @@ + +(* $Id$ *) + +(*i*) +open Pp +open Names +open Term +(*i*) + +val gencompr : path_kind -> Coqast.t -> std_ppcmds +val gentermpr : path_kind -> 'a assumptions -> constr -> std_ppcmds +val gentacpr : Coqast.t -> std_ppcmds + +val print_arguments : bool ref +val print_casts : bool ref +val print_emacs : bool ref +val with_implicits : ('a -> 'b) -> 'a -> 'b diff --git a/parsing/termast.mli b/parsing/termast.mli new file mode 100644 index 000000000..0314d5494 --- /dev/null +++ b/parsing/termast.mli @@ -0,0 +1,17 @@ + +(* $Id$ *) + +(*i*) +open Term +open Names +(*i*) + +val print_implicits : bool ref + +val bdize : bool -> unit assumptions -> constr -> Coqast.t +val bdize_no_casts : bool -> unit assumptions -> constr -> Coqast.t + +(* 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 diff --git a/pretyping/class.mli b/pretyping/class.mli new file mode 100644 index 000000000..cab7a15d2 --- /dev/null +++ b/pretyping/class.mli @@ -0,0 +1,2 @@ + +(* $Id$ *) diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli new file mode 100644 index 000000000..cab7a15d2 --- /dev/null +++ b/pretyping/evarconv.mli @@ -0,0 +1,2 @@ + +(* $Id$ *) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli new file mode 100644 index 000000000..cab7a15d2 --- /dev/null +++ b/pretyping/evarutil.mli @@ -0,0 +1,2 @@ + +(* $Id$ *) diff --git a/pretyping/multcase.mli b/pretyping/multcase.mli new file mode 100644 index 000000000..cab7a15d2 --- /dev/null +++ b/pretyping/multcase.mli @@ -0,0 +1,2 @@ + +(* $Id$ *) diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli new file mode 100644 index 000000000..cab7a15d2 --- /dev/null +++ b/pretyping/pretyping.mli @@ -0,0 +1,2 @@ + +(* $Id$ *) diff --git a/pretyping/record.mli b/pretyping/record.mli new file mode 100644 index 000000000..cab7a15d2 --- /dev/null +++ b/pretyping/record.mli @@ -0,0 +1,2 @@ + +(* $Id$ *) |