diff options
| author | herbelin | 2000-10-18 11:07:12 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-18 11:07:12 +0000 |
| commit | d6ffb0af8f4ec4e034692ec71d443f90520543fd (patch) | |
| tree | 37f24ff8666da896cc156bb01c90f04dfdbf7f50 /parsing/astterm.mli | |
| parent | 130e33deecba750bd0bd4bec16d53a04b039915d (diff) | |
Nettoyage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@717 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/astterm.mli')
| -rw-r--r-- | parsing/astterm.mli | 38 |
1 files changed, 5 insertions, 33 deletions
diff --git a/parsing/astterm.mli b/parsing/astterm.mli index 0521b05951..71f1b03bdc 100644 --- a/parsing/astterm.mli +++ b/parsing/astterm.mli @@ -50,6 +50,11 @@ val interp_constrpattern_gen : val interp_constrpattern : 'a evar_map -> env -> Coqast.t -> int list * constr_pattern +(*s Globalization of AST quotations (mainly used to get statically + bound idents in grammar or pretty-printing rules) *) +val globalize_constr : Coqast.t -> Coqast.t +val globalize_ast : Coqast.t -> Coqast.t + (* Translation rules from V6 to V7: constr_of_com_casted -> interp_casted_constr @@ -59,36 +64,3 @@ rawconstr_of_com -> interp_rawconstr [+ env instead of sign] type_of_com -> typed_type_of_com Evd.empty constr_of_com1 true -> interp_type *) - -(*i For debug (or obsolete) -val dbize_op : CoqAst.loc -> string -> CoqAst.t list -> constr list -> constr -val dbize : unit assumptions -> CoqAst.t -> constr - -val dbize_cci : 'c evar_map -> unit assumptions -> Coqast.t -> rawconstr -val absolutize_cci : 'c evar_map -> unit assumptions -> constr -> constr - -val dbize_fw : 'c evar_map -> unit assumptions -> Coqast.t -> rawconstr -val absolutize_fw : 'c evar_map -> unit assumptions -> constr -> constr -val raw_fconstr_of_com : - 'c evar_map -> 'a assumptions -> Coqast.t -> rawconstr -val fconstr_of_com : 'a evar_map -> env -> Coqast.t -> constr -val fconstr_of_com_sort : 'a evar_map -> env -> Coqast.t -> constr - -val raw_constr_of_compattern : - 'c evar_map -> 'a assumptions -> Coqast.t -> rawconstr - -*) -val globalize_constr : Coqast.t -> Coqast.t -(* -val globalize_ast : Coqast.t -> Coqast.t - -(* Typing with Trad, and re-checking with Mach *) -val fconstruct :'c evar_map -> context -> Coqast.t -> unsafe_judgment -val fconstruct_type : 'c evar_map -> context -> Coqast.t -> typed_type - -(* Typing, re-checking with universes constraints *) -val fconstruct_with_univ : - 'a evar_map -> context -> Coqast.t -> unsafe_judgment - -i*) - |