diff options
| author | letouzey | 2012-05-29 11:08:50 +0000 |
|---|---|---|
| committer | letouzey | 2012-05-29 11:08:50 +0000 |
| commit | 392300a73bc4e57d2be865d9a8d77c608ef02f59 (patch) | |
| tree | 44b4f39e7f92f29f4626d4aa8265fe68eb129111 /parsing/prettyp.ml | |
| parent | a936f2e879ac1f9b2e7e9d8a5376469e3d53c606 (diff) | |
New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/prettyp.ml')
| -rw-r--r-- | parsing/prettyp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 5dbef1fe5c..d90e655b14 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -44,7 +44,7 @@ type object_pr = { print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; print_context : bool -> int option -> Lib.library_segment -> std_ppcmds; print_typed_value_in_env : Environ.env -> Term.constr * Term.types -> Pp.std_ppcmds; - print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Topconstr.constr_expr -> unsafe_judgment -> std_ppcmds; + print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds; } let gallina_print_module = print_module @@ -435,7 +435,7 @@ let gallina_print_constant_with_infos sp = let gallina_print_syntactic_def kn = let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn and (vars,a) = Syntax_def.search_syntactic_definition kn in - let c = Topconstr.glob_constr_of_aconstr dummy_loc a in + let c = Topconstr.glob_constr_of_notation_constr dummy_loc a in hov 2 (hov 4 (str "Notation " ++ pr_qualid qid ++ |