diff options
Diffstat (limited to 'plugins')
52 files changed, 273 insertions, 203 deletions
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index e6abf1ccf0..f904aa3e68 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -120,7 +120,7 @@ val term_equal : term -> term -> bool val constr_of_term : term -> constr -val debug : (unit -> Pp.std_ppcmds) -> unit +val debug : (unit -> Pp.t) -> unit val forest : state -> forest @@ -169,7 +169,7 @@ val find_instances : state -> (quant_eq * int array) list val execute : bool -> state -> explanation option -val pr_idx_term : forest -> int -> Pp.std_ppcmds +val pr_idx_term : forest -> int -> Pp.t val empty_forest: unit -> forest diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index d6342b59c6..356bad98ba 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -9,30 +9,29 @@ open Names open Globnames open Miniml -open Pp (** By default, in module Format, you can do horizontal placing of blocks even if they include newlines, as long as the number of chars in the blocks are less that a line length. To avoid this awkward situation, we attach a big virtual size to [fnl] newlines. *) -val fnl : unit -> std_ppcmds -val fnl2 : unit -> std_ppcmds -val space_if : bool -> std_ppcmds +val fnl : unit -> Pp.t +val fnl2 : unit -> Pp.t +val space_if : bool -> Pp.t -val pp_par : bool -> std_ppcmds -> std_ppcmds +val pp_par : bool -> Pp.t -> Pp.t (** [pp_apply] : a head part applied to arguments, possibly with parenthesis *) -val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds +val pp_apply : Pp.t -> bool -> Pp.t list -> Pp.t (** Same as [pp_apply], but with also protection of the head by parenthesis *) -val pp_apply2 : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds +val pp_apply2 : Pp.t -> bool -> Pp.t list -> Pp.t -val pp_tuple_light : (bool -> 'a -> std_ppcmds) -> 'a list -> std_ppcmds -val pp_tuple : ('a -> std_ppcmds) -> 'a list -> std_ppcmds -val pp_boxed_tuple : ('a -> std_ppcmds) -> 'a list -> std_ppcmds +val pp_tuple_light : (bool -> 'a -> Pp.t) -> 'a list -> Pp.t +val pp_tuple : ('a -> Pp.t) -> 'a list -> Pp.t +val pp_boxed_tuple : ('a -> Pp.t) -> 'a list -> Pp.t -val pr_binding : Id.t list -> std_ppcmds +val pr_binding : Id.t list -> Pp.t val rename_id : Id.t -> Id.Set.t -> Id.t @@ -80,4 +79,4 @@ val mk_ind : string -> string -> MutInd.t val is_native_char : ml_ast -> bool val get_native_char : ml_ast -> char -val pp_native_char : ml_ast -> std_ppcmds +val pp_native_char : ml_ast -> Pp.t diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 7d69cbff1f..89c2a0ae30 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -132,7 +132,7 @@ let rec add_labels mp = function exception Impossible let check_arity env cb = - let t = Typeops.type_of_constant_type env cb.const_type in + let t = cb.const_type in if Reduction.is_arity env t then raise Impossible let check_fix env cb i = @@ -175,26 +175,32 @@ let factor_fix env l cb msb = (hack proposed by Elie) *) -let expand_mexpr env mp me = +let expand_mexpr env mpo me = let inl = Some (Flags.get_inline_level()) in - Mod_typing.translate_mse env (Some mp) inl me + Mod_typing.translate_mse env mpo inl me -(** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def]. - To check with Elie. *) - -let rec mp_of_mexpr = function - | MEident mp -> mp - | MEwith (seb,_) -> mp_of_mexpr seb - | _ -> assert false +let expand_modtype env mp me = + let inl = Some (Flags.get_inline_level()) in + Mod_typing.translate_modtype env mp inl ([],me) let no_delta = Mod_subst.empty_delta_resolver -let env_for_mtb_with_def env mp me idl = +let flatten_modtype env mp me_alg struc_opt = + match struc_opt with + | Some me -> me, no_delta + | None -> + let mtb = expand_modtype env mp me_alg in + mtb.mod_type, mtb.mod_delta + +(** Ad-hoc update of environment, inspired by [Mod_typing.check_with_aux_def]. +*) + +let env_for_mtb_with_def env mp me reso idl = let struc = Modops.destr_nofunctor me in let l = Label.of_id (List.hd idl) in let spot = function (l',SFBconst _) -> Label.equal l l' | _ -> false in let before = fst (List.split_when spot struc) in - Modops.add_structure mp before no_delta env + Modops.add_structure mp before reso env let make_cst resolver mp l = Mod_subst.constant_of_delta_kn resolver (KerName.make2 mp l) @@ -234,20 +240,24 @@ let rec extract_structure_spec env mp reso = function [extract_mexpression_spec] should come from a [mod_type_alg] field. This way, any encountered [MEident] should be a true module type. *) -and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with +and extract_mexpr_spec env mp1 (me_struct_o,me_alg) = match me_alg with | MEident mp -> Visit.add_mp_all mp; MTident mp | MEwith(me',WithDef(idl,(c,ctx)))-> - let env' = env_for_mtb_with_def env (mp_of_mexpr me') me_struct idl in - let mt = extract_mexpr_spec env mp1 (me_struct,me') in + let me_struct,delta = flatten_modtype env mp1 me' me_struct_o in + let env' = env_for_mtb_with_def env mp1 me_struct delta idl in + let mt = extract_mexpr_spec env mp1 (None,me') in (match extract_with_type env' c with (* cb may contain some kn *) | None -> mt - | Some (vl,typ) -> MTwith(mt,ML_With_type(idl,vl,typ))) + | Some (vl,typ) -> + type_iter_references Visit.add_ref typ; + MTwith(mt,ML_With_type(idl,vl,typ))) | MEwith(me',WithMod(idl,mp))-> Visit.add_mp_all mp; - MTwith(extract_mexpr_spec env mp1 (me_struct,me'), ML_With_module(idl,mp)) + MTwith(extract_mexpr_spec env mp1 (None,me'), ML_With_module(idl,mp)) | MEapply _ -> (* No higher-order module type in OCaml : we use the expanded version *) - extract_msignature_spec env mp1 no_delta (*TODO*) me_struct + let me_struct,delta = flatten_modtype env mp1 me_alg me_struct_o in + extract_msignature_spec env mp1 delta me_struct and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with | MoreFunctor (mbid, mtb, me_alg') -> @@ -258,8 +268,8 @@ and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with let mp = MPbound mbid in let env' = Modops.add_module_type mp mtb env in MTfunsig (mbid, extract_mbody_spec env mp mtb, - extract_mexpression_spec env' mp1 (me_struct',me_alg')) - | NoFunctor m -> extract_mexpr_spec env mp1 (me_struct,m) + extract_mexpression_spec env' mp1 (me_struct',me_alg')) + | NoFunctor m -> extract_mexpr_spec env mp1 (Some me_struct,m) and extract_msignature_spec env mp1 reso = function | NoFunctor struc -> @@ -335,7 +345,7 @@ and extract_mexpr env mp = function (* In Haskell/Scheme, we expand everything. For now, we also extract everything, dead code will be removed later (see [Modutil.optimize_struct]. *) - let sign,_,delta,_ = expand_mexpr env mp me in + let sign,_,delta,_ = expand_mexpr env (Some mp) me in extract_msignature env mp delta ~all:true sign | MEident mp -> if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false; @@ -685,3 +695,35 @@ let structure_for_compute c = let struc = optimize_struct (refs,[]) (mono_environment refs []) in let flatstruc = List.map snd (List.flatten (List.map snd struc)) in flatstruc, ast, mlt + +(* For the test-suite : + extraction to a temporary file + run ocamlc on it *) + +let compile f = + try + let args = ["ocamlc";"-I";Filename.dirname f;"-c";f^"i";f] in + let res = CUnix.sys_command (Envars.ocamlfind ()) args in + match res with + | Unix.WEXITED 0 -> () + | Unix.WEXITED n | Unix.WSIGNALED n | Unix.WSTOPPED n -> + CErrors.user_err + Pp.(str "Compilation of file " ++ str f ++ + str " failed with exit code " ++ int n) + with Unix.Unix_error (e,_,_) -> + CErrors.user_err + Pp.(str "Compilation of file " ++ str f ++ + str " failed with error " ++ str (Unix.error_message e)) + +let remove f = + if Sys.file_exists f then Sys.remove f + +let extract_and_compile l = + if lang () != Ocaml then + CErrors.user_err (Pp.str "This command only works with OCaml extraction"); + let f = Filename.temp_file "testextraction" ".ml" in + let () = full_extraction (Some f) l in + let () = compile f in + let () = remove f; remove (f^"i") in + let base = Filename.chop_suffix f ".ml" in + let () = remove (base^".cmo"); remove (base^".cmi") in + Feedback.msg_notice (str "Extracted code successfully compiled") diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index f289b63ad4..5769ff1176 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -17,6 +17,10 @@ val full_extraction : string option -> reference list -> unit val separate_extraction : reference list -> unit val extraction_library : bool -> Id.t -> unit +(* For the test-suite : extraction to a temporary file + ocamlc on it *) + +val extract_and_compile : reference list -> unit + (* For debug / external output via coqtop.byte + Drop : *) val mono_environment : @@ -25,7 +29,7 @@ val mono_environment : (* Used by the Relation Extraction plugin *) val print_one_decl : - Miniml.ml_structure -> ModPath.t -> Miniml.ml_decl -> Pp.std_ppcmds + Miniml.ml_structure -> ModPath.t -> Miniml.ml_decl -> Pp.t (* Used by Extraction Compute *) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 3661faadab..7644b49ceb 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -295,7 +295,11 @@ let rec extract_type env db j c args = | Ind ((kn,i),u) -> let s = (extract_ind env kn).ind_packets.(i).ip_sign in extract_type_app env db (IndRef (kn,i),s) args - | Case _ | Fix _ | CoFix _ | Proj _ -> Tunknown + | Proj (p,t) -> + (* Let's try to reduce, if it hasn't already been done. *) + if Projection.unfolded p then Tunknown + else extract_type env db j (Term.mkProj (Projection.unfold p, t)) args + | Case _ | Fix _ | CoFix _ -> Tunknown | _ -> assert false (*s Auxiliary function dealing with type application. @@ -518,7 +522,7 @@ and mlt_env env r = match r with match lookup_typedef kn cb with | Some _ as o -> o | None -> - let typ = Typeops.type_of_constant_type env cb.const_type + let typ = cb.const_type (* FIXME not sure if we should instantiate univs here *) in match flag_of_type env typ with | Info,TypeScheme -> @@ -543,7 +547,7 @@ let record_constant_type env kn opt_typ = | Some schema -> schema | None -> let typ = match opt_typ with - | None -> Typeops.type_of_constant_type env cb.const_type + | None -> cb.const_type | Some typ -> typ in let mlt = extract_type env [] 1 typ [] in @@ -969,7 +973,7 @@ let extract_fixpoint env vkn (fi,ti,ci) = let extract_constant env kn cb = let r = ConstRef kn in - let typ = Typeops.type_of_constant_type env cb.const_type in + let typ = cb.const_type in let warn_info () = if not (is_custom r) then add_info_axiom r in let warn_log () = if not (constant_has_body cb) then add_log_axiom r in @@ -1025,7 +1029,7 @@ let extract_constant env kn cb = let extract_constant_spec env kn cb = let r = ConstRef kn in - let typ = Typeops.type_of_constant_type env cb.const_type in + let typ = cb.const_type in try match flag_of_type env typ with | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype)) diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 4372ea557b..23452febdc 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Grammar_API.Pcoq.Prim +open Pcoq.Prim DECLARE PLUGIN "extraction_plugin" @@ -65,6 +65,10 @@ VERNAC COMMAND EXTEND Extraction CLASSIFIED AS QUERY (* Monolithic extraction to a file *) | [ "Extraction" string(f) ne_global_list(l) ] -> [ full_extraction (Some f) l ] + +(* Extraction to a temporary file and OCaml compilation *) +| [ "Extraction" "TestCompile" ne_global_list(l) ] + -> [ extract_and_compile l ] END VERNAC COMMAND EXTEND SeparateExtraction CLASSIFIED AS QUERY diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index be8282da06..edebba49df 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -8,7 +8,6 @@ (*s Target language for extraction: a core ML called MiniML. *) -open Pp open Names open Globnames @@ -205,19 +204,19 @@ type language_descr = { file_naming : ModPath.t -> string; (* the second argument is a comment to add to the preamble *) preamble : - Id.t -> std_ppcmds option -> ModPath.t list -> unsafe_needs -> - std_ppcmds; - pp_struct : ml_structure -> std_ppcmds; + Id.t -> Pp.t option -> ModPath.t list -> unsafe_needs -> + Pp.t; + pp_struct : ml_structure -> Pp.t; (* Concerning a possible interface file *) sig_suffix : string option; (* the second argument is a comment to add to the preamble *) sig_preamble : - Id.t -> std_ppcmds option -> ModPath.t list -> unsafe_needs -> - std_ppcmds; - pp_sig : ml_signature -> std_ppcmds; + Id.t -> Pp.t option -> ModPath.t list -> unsafe_needs -> + Pp.t; + pp_sig : ml_signature -> Pp.t; (* for an isolated declaration print *) - pp_decl : ml_decl -> std_ppcmds; + pp_decl : ml_decl -> Pp.t; } diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index f1bcde2f3f..a4c2bcd883 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -120,7 +120,6 @@ let rec mgu = function mgu (a, a'); mgu (b, b') | Tglob (r,l), Tglob (r',l') when Globnames.eq_gr r r' -> List.iter mgu (List.combine l l') - | (Tdummy _, _ | _, Tdummy _) when lang() == Haskell -> () | Tdummy _, Tdummy _ -> () | Tvar i, Tvar j when Int.equal i j -> () | Tvar' i, Tvar' j when Int.equal i j -> () @@ -1052,6 +1051,7 @@ let rec simpl o = function | MLmagic(MLcase(typ,e,br)) -> let br' = Array.map (fun (ids,p,c) -> (ids,p,MLmagic c)) br in simpl o (MLcase(typ,e,br')) + | MLmagic(MLdummy _ as e) when lang () == Haskell -> e | MLmagic(MLexn _ as e) -> e | a -> ast_map (simpl o) a diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index a896a8d037..1e0c331901 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -17,10 +17,15 @@ open Mlutil (*S Functions upon ML modules. *) +(** Note: a syntax like [(F M) with ...] is actually legal, see for instance + bug #4720. Hence the code below tries to handle [MTsig], maybe not in + a perfect way, but that should be enough for the use of [se_iter] below. *) + let rec msid_of_mt = function | MTident mp -> mp + | MTsig(mp,_) -> mp | MTwith(mt,_)-> msid_of_mt mt - | _ -> anomaly ~label:"extraction" (Pp.str "the With operator isn't applied to a name.") + | MTfunsig _ -> assert false (* A functor cannot be inside a MTwith *) (*s Apply some functions upon all [ml_decl] and [ml_spec] found in a [ml_structure]. *) @@ -36,7 +41,7 @@ let se_iter do_decl do_spec do_mp = List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl' in let r = ConstRef (Constant.make2 mp_w (Label.of_id l')) in - mt_iter mt; do_decl (Dtype(r,l,t)) + mt_iter mt; do_spec (Stype(r,l,Some t)) | MTwith (mt,ML_With_module(idl,mp))-> let mp_mt = msid_of_mt mt in let mp_w = diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli index ad60b58d5d..17a6e8db6f 100644 --- a/plugins/extraction/modutil.mli +++ b/plugins/extraction/modutil.mli @@ -17,6 +17,7 @@ val struct_type_search : (ml_type -> bool) -> ml_structure -> bool type do_ref = global_reference -> unit +val type_iter_references : do_ref -> ml_type -> unit val ast_iter_references : do_ref -> do_ref -> do_ref -> ml_ast -> unit val decl_iter_references : do_ref -> do_ref -> do_ref -> ml_decl -> unit val spec_iter_references : do_ref -> do_ref -> do_ref -> ml_spec -> unit diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 2b3007f025..7e47d0bc81 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -191,7 +191,7 @@ val find_custom_match : ml_branch array -> string val extraction_language : lang -> unit val extraction_inline : bool -> reference list -> unit -val print_extraction_inline : unit -> Pp.std_ppcmds +val print_extraction_inline : unit -> Pp.t val reset_extraction_inline : unit -> unit val extract_constant_inline : bool -> reference -> string list -> string -> unit @@ -206,7 +206,7 @@ val extraction_implicit : reference -> int_or_id list -> unit val extraction_blacklist : Id.t list -> unit val reset_extraction_blacklist : unit -> unit -val print_extraction_blacklist : unit -> Pp.std_ppcmds +val print_extraction_blacklist : unit -> Pp.t diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index c001ee3829..1e7da3250b 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Grammar_API open Ltac_plugin open Formula open Sequent diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index 0a2e84bb83..ca6079c8b0 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -57,4 +57,4 @@ val extend_with_ref_list : Environ.env -> Evd.evar_map -> global_reference list val extend_with_auto_hints : Environ.env -> Evd.evar_map -> Hints.hint_db_name list -> t -> t * Evd.evar_map -val print_cmap: global_reference list CM.t -> Pp.std_ppcmds +val print_cmap: global_reference list CM.t -> Pp.t diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 15ab396e31..5f6d783598 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -821,8 +821,9 @@ let build_proof | Fix _ | CoFix _ -> user_err Pp.(str ( "Anonymous local (co)fixpoints are not handled yet")) + | Proj _ -> user_err Pp.(str "Prod") - | Prod _ -> user_err Pp.(str "Prod") + | Prod _ -> do_finalize dyn_infos g | LetIn _ -> let new_infos = { dyn_infos with diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index c495703eeb..16d9f200f3 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) (*i camlp4deps: "grammar/grammar.cma" i*) -open Grammar_API open Ltac_plugin open Util open Pp diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 379c83b245..8555a0b226 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -32,6 +32,14 @@ type binder_type = type glob_context = (binder_type*glob_constr) list + +let rec solve_trivial_holes pat_as_term e = + match pat_as_term.CAst.v,e.CAst.v with + | GHole _,_ -> e + | GApp(fp,argsp),GApp(fe,argse) when glob_constr_eq fp fe -> + CAst.make (GApp((solve_trivial_holes fp fe),List.map2 solve_trivial_holes argsp argse)) + | _,_ -> pat_as_term + (* compose_glob_context [(bt_1,n_1,t_1);......] rt returns b_1(n_1,t_1,.....,bn(n_k,t_k,rt)) where the b_i's are the @@ -226,7 +234,12 @@ let combine_lam n t b = compose_glob_context b.context b.value ) } - +let combine_prod2 n t b = + { + context = []; + value = mkGProd(n, compose_glob_context t.context t.value, + compose_glob_context b.context b.value ) + } let combine_prod n t b = { context = t.context@((Prod n,t.value)::b.context); value = b.value} @@ -604,7 +617,9 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let t_res = build_entry_lc env funnames avoid t in let new_env = raw_push_named (n,None,t) env in let b_res = build_entry_lc new_env funnames avoid b in - combine_results (combine_prod n) t_res b_res + if List.length t_res.result = 1 && List.length b_res.result = 1 + then combine_results (combine_prod2 n) t_res b_res + else combine_results (combine_prod n) t_res b_res | GLetIn(n,v,typ,b) -> (* we first compute the list of constructor corresponding to the body of the function, @@ -806,6 +821,12 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve let typ_as_constr = EConstr.of_constr typ_as_constr in let typ = Detyping.detype false [] new_env (Evd.from_env env) typ_as_constr in let pat_as_term = pattern_to_term pat in + (* removing trivial holes *) + let pat_as_term = solve_trivial_holes pat_as_term e in + (* observe (str "those_pattern_preconds" ++ spc () ++ *) + (* str "pat" ++ spc () ++ pr_glob_constr pat_as_term ++ spc ()++ *) + (* str "e" ++ spc () ++ pr_glob_constr e ++spc ()++ *) + (* str "typ_as_constr" ++ spc () ++ pr_lconstr typ_as_constr); *) List.fold_right (fun id acc -> if Id.Set.mem id this_pat_ids diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 7cb35838c7..003bb4e30d 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -708,9 +708,6 @@ let expand_as = in expand_as Id.Map.empty - - - (* [resolve_and_replace_implicits ?expected_type env sigma rt] solves implicits of [rt] w.r.t. [env] and [sigma] and then replace them by their solution *) @@ -749,6 +746,30 @@ If someone knows how to prevent solved existantial removal in understand, pleas Detyping.detype false [] env ctx (EConstr.of_constr (f c)) | Evar_empty -> rt (* the hole was not solved : we do nothing *) ) + | (GHole(BinderType na,_,_)) -> (* we only want to deal with implicit arguments *) + ( + let res = + try (* we scan the new evar map to find the evar corresponding to this hole (by looking the source *) + Evd.fold (* to simulate an iter *) + (fun _ evi _ -> + match evi.evar_source with + | (loc_evi,BinderType na') -> + if Name.equal na na' && rt.CAst.loc = loc_evi then raise (Found evi) + | _ -> () + ) + ctx + (); + (* the hole was not solved : we do nothing *) + rt + with Found evi -> (* we found the evar corresponding to this hole *) + match evi.evar_body with + | Evar_defined c -> + (* we just have to lift the solution in glob_term *) + Detyping.detype false [] env ctx (EConstr.of_constr (f c)) + | Evar_empty -> rt (* the hole was not solved : we d when falseo nothing *) + in + res + ) | _ -> Glob_ops.map_glob_constr change rt in change rt diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 863c9dc8d5..89537ad3f6 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -857,7 +857,7 @@ let make_graph (f_ref:global_reference) = with_full_print (fun () -> (Constrextern.extern_constr false env sigma body, Constrextern.extern_type false env sigma - ((*FIXME*) Typeops.type_of_constant_type env c_body.const_type) + ((*FIXME*) c_body.const_type) ) ) () diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index 7a60da44fb..93e03852ec 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -1,8 +1,8 @@ open Misctypes -val warn_cannot_define_graph : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit +val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit -val warn_cannot_define_principle : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit +val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit val do_generate_principle : bool -> diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 5e425cd18a..2e2ced790e 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -1,5 +1,4 @@ open Names -open Pp (* The mk_?_id function build different name w.r.t. a function @@ -11,7 +10,7 @@ val mk_complete_id : Id.t -> Id.t val mk_equation_id : Id.t -> Id.t -val msgnl : std_ppcmds -> unit +val msgnl : Pp.t -> unit val fresh_id : Id.t list -> string -> Id.t val fresh_name : Id.t list -> string -> Name.t @@ -24,7 +23,7 @@ val id_of_name : Name.t -> Id.t val locate_ind : Libnames.reference -> inductive val locate_constant : Libnames.reference -> Constant.t val locate_with_msg : - Pp.std_ppcmds -> (Libnames.reference -> 'a) -> + Pp.t -> (Libnames.reference -> 'a) -> Libnames.reference -> 'a val filter_map : ('a -> bool) -> ('a -> 'b) -> 'a list -> 'b list @@ -89,8 +88,8 @@ val update_Function : function_info -> unit (** debugging *) -val pr_info : function_info -> Pp.std_ppcmds -val pr_table : unit -> Pp.std_ppcmds +val pr_info : function_info -> Pp.t +val pr_table : unit -> Pp.t (* val function_debug : bool ref *) diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 72c6f90900..6097951330 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Grammar_API open Pp open Genarg open Stdarg diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index 419c5e8c45..b06f35ddc4 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Grammar_API open Tacexpr open Names open Constrexpr @@ -15,13 +14,13 @@ open Misctypes val wit_orient : bool Genarg.uniform_genarg_type val orient : bool Pcoq.Gram.entry -val pr_orient : bool -> Pp.std_ppcmds +val pr_orient : bool -> Pp.t val wit_rename : (Id.t * Id.t) Genarg.uniform_genarg_type val occurrences : (int list or_var) Pcoq.Gram.entry val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg_type -val pr_occurrences : int list or_var -> Pp.std_ppcmds +val pr_occurrences : int list or_var -> Pp.t val occurrences_of : int list -> Locus.occurrences val wit_natural : int Genarg.uniform_genarg_type @@ -56,7 +55,7 @@ type place = Id.t gen_place val wit_hloc : (loc_place, loc_place, place) Genarg.genarg_type val hloc : loc_place Pcoq.Gram.entry -val pr_hloc : loc_place -> Pp.std_ppcmds +val pr_hloc : loc_place -> Pp.t val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry val wit_by_arg_tac : @@ -65,8 +64,8 @@ val wit_by_arg_tac : Geninterp.Val.t option) Genarg.genarg_type val pr_by_arg_tac : - (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) -> - raw_tactic_expr option -> Pp.std_ppcmds + (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.t) -> + raw_tactic_expr option -> Pp.t val test_lpar_id_colon : unit Pcoq.Gram.entry diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 6d80ab5494..f3f2f27e9e 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Grammar_API open Pp open Genarg open Stdarg diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 4d13d89a49..301943a509 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Grammar_API open Pp open Genarg open Stdarg diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index cc052c8a20..2ea0f60ebc 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -8,8 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Grammar_API - DECLARE PLUGIN "ltac_plugin" open Util diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index 1935d560a4..1a2d895868 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -12,7 +12,6 @@ Syntax for the subtac terms and types. Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *) -open Grammar_API open Libnames open Constrexpr open Constrexpr_ops diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index 3c27b27475..c874f8d5a3 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -10,7 +10,6 @@ (* Syntax for rewriting with strategies *) -open Grammar_API open Names open Misctypes open Locus diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index e539b58674..d792d4ff7d 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Grammar_API open Pp open CErrors open Util diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml index 2adcf02e69..2c1b1067ea 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Grammar_API open Pcoq (* Main entry for extensions *) diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 794cb527f3..048dcc8e92 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -8,7 +8,6 @@ (** Ltac parsing entries *) -open Grammar_API open Loc open Names open Pcoq diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 327b347ec0..140cc33440 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -67,22 +67,22 @@ let declare_notation_tactic_pprule kn pt = prnotation_tab := KNmap.add kn pt !prnotation_tab type 'a raw_extra_genarg_printer = - (constr_expr -> std_ppcmds) -> - (constr_expr -> std_ppcmds) -> - (tolerability -> raw_tactic_expr -> std_ppcmds) -> - 'a -> std_ppcmds + (constr_expr -> Pp.t) -> + (constr_expr -> Pp.t) -> + (tolerability -> raw_tactic_expr -> Pp.t) -> + 'a -> Pp.t type 'a glob_extra_genarg_printer = - (glob_constr_and_expr -> std_ppcmds) -> - (glob_constr_and_expr -> std_ppcmds) -> - (tolerability -> glob_tactic_expr -> std_ppcmds) -> - 'a -> std_ppcmds + (glob_constr_and_expr -> Pp.t) -> + (glob_constr_and_expr -> Pp.t) -> + (tolerability -> glob_tactic_expr -> Pp.t) -> + 'a -> Pp.t type 'a extra_genarg_printer = - (EConstr.constr -> std_ppcmds) -> - (EConstr.constr -> std_ppcmds) -> - (tolerability -> Val.t -> std_ppcmds) -> - 'a -> std_ppcmds + (EConstr.constr -> Pp.t) -> + (EConstr.constr -> Pp.t) -> + (tolerability -> Val.t -> Pp.t) -> + 'a -> Pp.t let keyword x = tag_keyword (str x) let primitive x = tag_primitive (str x) @@ -96,7 +96,7 @@ type 'a extra_genarg_printer = | None -> assert false | Some Refl -> x - let rec pr_value lev v : std_ppcmds = + let rec pr_value lev v : Pp.t = if has_type v Val.typ_list then pr_sequence (fun x -> pr_value lev x) (unbox v Val.typ_list) else if has_type v Val.typ_opt then @@ -272,7 +272,7 @@ type 'a extra_genarg_printer = | Glbwit (OptArg wit) -> Some (Option.map (in_gen (glbwit wit)) arg) | _ -> None - let rec pr_any_arg : type l. (_ -> l generic_argument -> std_ppcmds) -> _ -> l generic_argument -> std_ppcmds = + let rec pr_any_arg : type l. (_ -> l generic_argument -> Pp.t) -> _ -> l generic_argument -> Pp.t = fun prtac symb arg -> match symb with | Extend.Uentry tag when is_genarg tag (genarg_tag arg) -> prtac (1, Any) arg | Extend.Ulist1 s | Extend.Ulist0 s -> @@ -599,18 +599,18 @@ type 'a extra_genarg_printer = "raw", "glob" and "typed" levels *) type 'a printer = { - pr_tactic : tolerability -> 'tacexpr -> std_ppcmds; - pr_constr : 'trm -> std_ppcmds; - pr_lconstr : 'trm -> std_ppcmds; - pr_dconstr : 'dtrm -> std_ppcmds; - pr_pattern : 'pat -> std_ppcmds; - pr_lpattern : 'pat -> std_ppcmds; - pr_constant : 'cst -> std_ppcmds; - pr_reference : 'ref -> std_ppcmds; - pr_name : 'nam -> std_ppcmds; - pr_generic : 'lev generic_argument -> std_ppcmds; - pr_extend : int -> ml_tactic_entry -> 'a gen_tactic_arg list -> std_ppcmds; - pr_alias : int -> KerName.t -> 'a gen_tactic_arg list -> std_ppcmds; + pr_tactic : tolerability -> 'tacexpr -> Pp.t; + pr_constr : 'trm -> Pp.t; + pr_lconstr : 'trm -> Pp.t; + pr_dconstr : 'dtrm -> Pp.t; + pr_pattern : 'pat -> Pp.t; + pr_lpattern : 'pat -> Pp.t; + pr_constant : 'cst -> Pp.t; + pr_reference : 'ref -> Pp.t; + pr_name : 'nam -> Pp.t; + pr_generic : 'lev generic_argument -> Pp.t; + pr_extend : int -> ml_tactic_entry -> 'a gen_tactic_arg list -> Pp.t; + pr_alias : int -> KerName.t -> 'a gen_tactic_arg list -> Pp.t; } constraint 'a = < diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 1127c98319..0bf9bc7f62 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -9,7 +9,6 @@ (** This module implements pretty-printers for tactic_expr syntactic objects and their subcomponents. *) -open Pp open Genarg open Geninterp open Names @@ -24,22 +23,22 @@ type 'a grammar_tactic_prod_item_expr = | TacNonTerm of ('a * Names.Id.t option) Loc.located type 'a raw_extra_genarg_printer = - (constr_expr -> std_ppcmds) -> - (constr_expr -> std_ppcmds) -> - (tolerability -> raw_tactic_expr -> std_ppcmds) -> - 'a -> std_ppcmds + (constr_expr -> Pp.t) -> + (constr_expr -> Pp.t) -> + (tolerability -> raw_tactic_expr -> Pp.t) -> + 'a -> Pp.t type 'a glob_extra_genarg_printer = - (glob_constr_and_expr -> std_ppcmds) -> - (glob_constr_and_expr -> std_ppcmds) -> - (tolerability -> glob_tactic_expr -> std_ppcmds) -> - 'a -> std_ppcmds + (glob_constr_and_expr -> Pp.t) -> + (glob_constr_and_expr -> Pp.t) -> + (tolerability -> glob_tactic_expr -> Pp.t) -> + 'a -> Pp.t type 'a extra_genarg_printer = - (EConstr.t -> std_ppcmds) -> - (EConstr.t -> std_ppcmds) -> - (tolerability -> Val.t -> std_ppcmds) -> - 'a -> std_ppcmds + (EConstr.t -> Pp.t) -> + (EConstr.t -> Pp.t) -> + (tolerability -> Val.t -> Pp.t) -> + 'a -> Pp.t val declare_extra_genarg_pprule : ('a, 'b, 'c) genarg_type -> @@ -57,61 +56,61 @@ type pp_tactic = { val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit val pr_with_occurrences : - ('a -> std_ppcmds) -> 'a Locus.with_occurrences -> std_ppcmds + ('a -> Pp.t) -> 'a Locus.with_occurrences -> Pp.t val pr_red_expr : - ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) -> - ('a,'b,'c) Genredexpr.red_expr_gen -> std_ppcmds + ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) -> + ('a,'b,'c) Genredexpr.red_expr_gen -> Pp.t val pr_may_eval : - ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> - ('c -> std_ppcmds) -> ('a,'b,'c) Genredexpr.may_eval -> std_ppcmds + ('a -> Pp.t) -> ('a -> Pp.t) -> ('b -> Pp.t) -> + ('c -> Pp.t) -> ('a,'b,'c) Genredexpr.may_eval -> Pp.t -val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds -val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds +val pr_and_short_name : ('a -> Pp.t) -> 'a and_short_name -> Pp.t +val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t val pr_in_clause : - ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds + ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t val pr_clauses : bool option -> - ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds + ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t -val pr_raw_generic : env -> rlevel generic_argument -> std_ppcmds +val pr_raw_generic : env -> rlevel generic_argument -> Pp.t -val pr_glb_generic : env -> glevel generic_argument -> std_ppcmds +val pr_glb_generic : env -> glevel generic_argument -> Pp.t val pr_raw_extend: env -> int -> - ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds + ml_tactic_entry -> raw_tactic_arg list -> Pp.t val pr_glob_extend: env -> int -> - ml_tactic_entry -> glob_tactic_arg list -> std_ppcmds + ml_tactic_entry -> glob_tactic_arg list -> Pp.t val pr_extend : - (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds + (Val.t -> Pp.t) -> int -> ml_tactic_entry -> Val.t list -> Pp.t -val pr_alias_key : Names.KerName.t -> std_ppcmds +val pr_alias_key : Names.KerName.t -> Pp.t -val pr_alias : (Val.t -> std_ppcmds) -> - int -> Names.KerName.t -> Val.t list -> std_ppcmds +val pr_alias : (Val.t -> Pp.t) -> + int -> Names.KerName.t -> Val.t list -> Pp.t -val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds +val pr_ltac_constant : Nametab.ltac_constant -> Pp.t -val pr_raw_tactic : raw_tactic_expr -> std_ppcmds +val pr_raw_tactic : raw_tactic_expr -> Pp.t -val pr_raw_tactic_level : tolerability -> raw_tactic_expr -> std_ppcmds +val pr_raw_tactic_level : tolerability -> raw_tactic_expr -> Pp.t -val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds +val pr_glob_tactic : env -> glob_tactic_expr -> Pp.t -val pr_atomic_tactic : env -> Evd.evar_map -> atomic_tactic_expr -> std_ppcmds +val pr_atomic_tactic : env -> Evd.evar_map -> atomic_tactic_expr -> Pp.t -val pr_hintbases : string list option -> std_ppcmds +val pr_hintbases : string list option -> Pp.t -val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds +val pr_auto_using : ('constr -> Pp.t) -> 'constr list -> Pp.t -val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds +val pr_match_pattern : ('a -> Pp.t) -> 'a match_pattern -> Pp.t -val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> - ('b, 'a) match_rule -> std_ppcmds +val pr_match_rule : bool -> ('a -> Pp.t) -> ('b -> Pp.t) -> + ('b, 'a) match_rule -> Pp.t -val pr_value : tolerability -> Val.t -> std_ppcmds +val pr_value : tolerability -> Val.t -> Pp.t val ltop : tolerability diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index bbd7834d58..75b665aad9 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1461,7 +1461,7 @@ let solve_constraints env (evars,cstrs) = let nf_zeta = Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) -exception RewriteFailure of Pp.std_ppcmds +exception RewriteFailure of Pp.t type result = (evar_map * constr option * types) option option diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 35205ac58a..23767c12f5 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -61,8 +61,8 @@ val strategy_of_ast : (glob_constr_and_expr, raw_red_expr) strategy_ast -> strat val map_strategy : ('a -> 'b) -> ('c -> 'd) -> ('a, 'c) strategy_ast -> ('b, 'd) strategy_ast -val pr_strategy : ('a -> Pp.std_ppcmds) -> ('b -> Pp.std_ppcmds) -> - ('a, 'b) strategy_ast -> Pp.std_ppcmds +val pr_strategy : ('a -> Pp.t) -> ('b -> Pp.t) -> + ('a, 'b) strategy_ast -> Pp.t (** Entry point for user-level "rewrite_strat" *) val cl_rewrite_clause_strat : strategy -> Id.t option -> unit Proofview.tactic diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 791b7f48db..cf676f598f 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Grammar_API open Pp open CErrors open Util diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index ccd44b914e..aa8f4efe65 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -8,7 +8,6 @@ (** Ltac toplevel command entries. *) -open Grammar_API open Vernacexpr open Tacexpr diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index df03c7b472..0554d43641 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Grammar_API open Pattern open Pp open Genredexpr diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index ad2e709085..e3a4d5c798 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Grammar_API -open Pp open Names open Tacexpr open Genarg @@ -56,7 +54,7 @@ val intern_hyp : glob_sign -> Id.t Loc.located -> Id.t Loc.located val intern_genarg : glob_sign -> raw_generic_argument -> glob_generic_argument (** printing *) -val print_ltac : Libnames.qualid -> std_ppcmds +val print_ltac : Libnames.qualid -> Pp.t (** Reduction expressions *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 7b054947b7..d3e625e73a 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Grammar_API open Constrintern open Patternops open Pp @@ -2001,7 +2000,7 @@ let lift f = (); fun ist x -> Ftactic.enter begin fun gl -> Ftactic.return (f ist env sigma x) end -let lifts f = (); fun ist x -> Ftactic.nf_enter begin fun gl -> +let lifts f = (); fun ist x -> Ftactic.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let (sigma, v) = f ist env sigma x in diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index c1ca854334..180fb2db40 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Grammar_API open Util open Tacexpr open Mod_subst diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index ef6362270a..2475e41f9d 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -58,16 +58,16 @@ val db_hyp_pattern_failure : val db_matching_failure : debug_info -> unit Proofview.NonLogical.t (** Prints an evaluation failure message for a rule *) -val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit Proofview.NonLogical.t +val db_eval_failure : debug_info -> Pp.t -> unit Proofview.NonLogical.t (** An exception handler *) -val explain_logic_error: exn -> Pp.std_ppcmds +val explain_logic_error: exn -> Pp.t (** For use in the Ltac debugger: some exception that are usually consider anomalies are acceptable because they are caught later in the process that is being debugged. One should not require from users that they report these anomalies. *) -val explain_logic_error_no_anomaly : exn -> Pp.std_ppcmds +val explain_logic_error_no_anomaly : exn -> Pp.t (** Prints a logic failure message for a rule *) val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t @@ -77,4 +77,4 @@ val db_breakpoint : debug_info -> Id.t Loc.located message_token list -> unit Proofview.NonLogical.t val extract_ltac_trace : - ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.std_ppcmds option Loc.located + ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.t option Loc.located diff --git a/plugins/ltac/tactic_option.mli b/plugins/ltac/tactic_option.mli index dd91944d48..95cd243ec8 100644 --- a/plugins/ltac/tactic_option.mli +++ b/plugins/ltac/tactic_option.mli @@ -12,4 +12,4 @@ open Vernacexpr val declare_tactic_option : ?default:Tacexpr.glob_tactic_expr -> string -> (* put *) (locality_flag -> glob_tactic_expr -> unit) * (* get *) (unit -> locality_flag * unit Proofview.tactic) * - (* print *) (unit -> Pp.std_ppcmds) + (* print *) (unit -> Pp.t) diff --git a/plugins/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli index e0c09f394c..86231cf199 100644 --- a/plugins/rtauto/proof_search.mli +++ b/plugins/rtauto/proof_search.mli @@ -38,9 +38,9 @@ val branching: state -> state list val success: state -> bool -val pp: state -> Pp.std_ppcmds +val pp: state -> Pp.t -val pr_form : form -> Pp.std_ppcmds +val pr_form : form -> Pp.t val reset_info : unit -> unit diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index 6c82346bca..05ab8ab326 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Grammar_API open Ltac_plugin open Pp open Util diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 608b778e4f..799e969ae2 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open Grammar_API open Util open Names open Evd diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 4b045e989a..2eadd5f26c 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -41,7 +41,7 @@ val nohint : 'a ssrhint (******************************** misc ************************************) -val errorstrm : Pp.std_ppcmds -> 'a +val errorstrm : Pp.t -> 'a val anomaly : string -> 'a val array_app_tl : 'a array -> 'a list -> 'a list diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 228444b82e..ce23bb2b30 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open Grammar_API open Names open Pp open Pcoq diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index c93e104056..88beeaa711 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -8,8 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open Grammar_API - val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type val pr_ssrtacarg : 'a -> 'b -> (int * Ppextend.parenRelation -> 'c) -> 'c @@ -18,5 +16,5 @@ val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type val pr_ssrtclarg : 'a -> 'b -> (int * Ppextend.parenRelation -> 'c -> 'd) -> 'c -> 'd -val add_genarg : string -> ('a -> Pp.std_ppcmds) -> 'a Genarg.uniform_genarg_type +val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli index 5c68872b75..f231068265 100644 --- a/plugins/ssr/ssrprinters.mli +++ b/plugins/ssr/ssrprinters.mli @@ -11,16 +11,16 @@ open Ssrast val pp_term : - Goal.goal Evd.sigma -> EConstr.constr -> Pp.std_ppcmds + Goal.goal Evd.sigma -> EConstr.constr -> Pp.t -val pr_spc : unit -> Pp.std_ppcmds -val pr_bar : unit -> Pp.std_ppcmds +val pr_spc : unit -> Pp.t +val pr_bar : unit -> Pp.t val pr_list : - (unit -> Pp.std_ppcmds) -> ('a -> Pp.std_ppcmds) -> 'a list -> Pp.std_ppcmds + (unit -> Pp.t) -> ('a -> Pp.t) -> 'a list -> Pp.t val pp_concat : - Pp.std_ppcmds -> - ?sep:Pp.std_ppcmds -> Pp.std_ppcmds list -> Pp.std_ppcmds + Pp.t -> + ?sep:Pp.t -> Pp.t list -> Pp.t val xInParens : ssrtermkind val xWithAt : ssrtermkind @@ -29,17 +29,17 @@ val xCpattern : ssrtermkind val pr_term : ssrtermkind * (Glob_term.glob_constr * Constrexpr.constr_expr option) -> - Pp.std_ppcmds + Pp.t -val pr_hyp : ssrhyp -> Pp.std_ppcmds +val pr_hyp : ssrhyp -> Pp.t -val prl_constr_expr : Constrexpr.constr_expr -> Pp.std_ppcmds -val prl_glob_constr : Glob_term.glob_constr -> Pp.std_ppcmds +val prl_constr_expr : Constrexpr.constr_expr -> Pp.t +val prl_glob_constr : Glob_term.glob_constr -> Pp.t val pr_guarded : - (string -> int -> bool) -> ('a -> Pp.std_ppcmds) -> 'a -> Pp.std_ppcmds + (string -> int -> bool) -> ('a -> Pp.t) -> 'a -> Pp.t -val pr_occ : ssrocc -> Pp.std_ppcmds +val pr_occ : ssrocc -> Pp.t -val ppdebug : Pp.std_ppcmds Lazy.t -> unit +val ppdebug : Pp.t Lazy.t -> unit diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index fbe3cd2b91..9c59d83d4e 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open Grammar_API open Names open Term open Termops diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 74519f6c54..f6300ab7e1 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -8,8 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open Grammar_API - (* Defining grammar rules with "xx" in it automatically declares keywords too, * we thus save the lexer to restore it at the end of the file *) let frozen_lexer = CLexer.get_keyword_state () ;; diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 0c09d7bfbf..8e2a1a7176 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -1,7 +1,6 @@ (* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -open Grammar_API open Goal open Genarg open Tacexpr @@ -16,7 +15,7 @@ open Term (** The type of context patterns, the patterns of the [set] tactic and [:] tactical. These are patterns that identify a precise subterm. *) type cpattern -val pr_cpattern : cpattern -> Pp.std_ppcmds +val pr_cpattern : cpattern -> Pp.t (** CS cpattern: (f _), (X in t), (t in X in t), (t as X in t) *) val cpattern : cpattern Pcoq.Gram.entry @@ -30,7 +29,7 @@ val wit_lcpattern : cpattern uniform_genarg_type These patterns also include patterns that identify all the subterms of a context (i.e. "in" prefix) *) type rpattern -val pr_rpattern : rpattern -> Pp.std_ppcmds +val pr_rpattern : rpattern -> Pp.t (** OS rpattern: f _, in t, X in t, in X in t, t in X in t, t as X in t *) val rpattern : rpattern Pcoq.Gram.entry @@ -51,7 +50,7 @@ type ('ident, 'term) ssrpattern = | E_As_X_In_T of 'term * 'ident * 'term type pattern = evar_map * (constr, constr) ssrpattern -val pp_pattern : pattern -> Pp.std_ppcmds +val pp_pattern : pattern -> Pp.t (** Extracts the redex and applies to it the substitution part of the pattern. @raise Anomaly if called on [In_T] or [In_X_In_T] *) @@ -116,7 +115,7 @@ val fill_occ_pattern : the T pattern above, and calls a continuation on its occurrences. *) type ssrdir = L2R | R2L -val pr_dir_side : ssrdir -> Pp.std_ppcmds +val pr_dir_side : ssrdir -> Pp.t (** a pattern for a term with wildcards *) type tpattern @@ -226,7 +225,7 @@ val loc_of_cpattern : cpattern -> Loc.t option val id_of_pattern : pattern -> Names.Id.t option val is_wildcard : cpattern -> bool val cpattern_of_id : Names.Id.t -> cpattern -val pr_constr_pat : constr -> Pp.std_ppcmds +val pr_constr_pat : constr -> Pp.t val pf_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma val pf_unsafe_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma |