From 368a25e4ef14512b00f5799e26c3f615bc540201 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 22 May 2018 00:07:26 +0200 Subject: [api] Misctypes removal: several moves: - move_location to proofs/logic. - intro_pattern_naming to Namegen. --- plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/glob_term_to_relation.ml | 1 - plugins/funind/glob_termops.ml | 11 +++++------ plugins/funind/indfun.ml | 4 ++-- plugins/funind/indfun.mli | 2 +- plugins/funind/invfun.ml | 6 +++--- plugins/funind/invfun.mli | 2 +- plugins/funind/recdef.ml | 2 +- 8 files changed, 14 insertions(+), 16 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 0a2741ad1..24d1a40c2 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -15,7 +15,7 @@ open Indfun_common open Indfun open Genarg open Stdarg -open Misctypes +open Tactypes open Pcoq open Pcoq.Prim open Pcoq.Constr diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 3ba3bafa4..6b9b10312 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -10,7 +10,6 @@ open Indfun_common open CErrors open Util open Glob_termops -open Misctypes module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index bb1587507..954fc3bab 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -5,7 +5,6 @@ open CErrors open Util open Names open Decl_kinds -open Misctypes (* Some basic functions to rebuild glob_constr @@ -18,7 +17,7 @@ let mkGLambda(n,t,b) = DAst.make @@ GLambda(n,Explicit,t,b) let mkGProd(n,t,b) = DAst.make @@ GProd(n,Explicit,t,b) let mkGLetIn(n,b,t,c) = DAst.make @@ GLetIn(n,b,t,c) let mkGCases(rto,l,brl) = DAst.make @@ GCases(RegularStyle,rto,l,brl) -let mkGHole () = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) +let mkGHole () = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Namegen.IntroAnonymous,None) (* Some basic functions to decompose glob_constrs @@ -109,7 +108,7 @@ let change_vars = | GHole _ as x -> x | GCast(b,c) -> GCast(change_vars mapping b, - Miscops.map_cast_type (change_vars mapping) c) + Glob_ops.map_cast_type (change_vars mapping) c) | GProj(p,c) -> GProj(p, change_vars mapping c) ) rt and change_vars_br mapping ({CAst.loc;v=(idl,patl,res)} as br) = @@ -290,7 +289,7 @@ let rec alpha_rt excluded rt = | GHole _ as rt -> rt | GCast (b,c) -> GCast(alpha_rt excluded b, - Miscops.map_cast_type (alpha_rt excluded) c) + Glob_ops.map_cast_type (alpha_rt excluded) c) | GApp(f,args) -> GApp(alpha_rt excluded f, List.map (alpha_rt excluded) args @@ -440,7 +439,7 @@ let replace_var_by_term x_id term = | GHole _ as rt -> rt | GCast(b,c) -> GCast(replace_var_by_pattern b, - Miscops.map_cast_type replace_var_by_pattern c) + Glob_ops.map_cast_type replace_var_by_pattern c) | GProj(p,c) -> GProj(p,replace_var_by_pattern c) ) x @@ -542,7 +541,7 @@ let expand_as = | GRec _ -> user_err Pp.(str "Not handled GRec") | GCast(b,c) -> GCast(expand_as map b, - Miscops.map_cast_type (expand_as map) c) + Glob_ops.map_cast_type (expand_as map) c) | GCases(sty,po,el,brl) -> GCases(sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, List.map (expand_as_br map) brl) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index efbd029e4..cd640eebd 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -10,7 +10,7 @@ open Libnames open Globnames open Glob_term open Declarations -open Misctypes +open Tactypes open Decl_kinds module RelDecl = Context.Rel.Declaration @@ -782,7 +782,7 @@ let rec add_args id new_args = CAst.map (function | CSort _ as b -> b | CCast(b1,b2) -> CCast(add_args id new_args b1, - Miscops.map_cast_type (add_args id new_args) b2) + Glob_ops.map_cast_type (add_args id new_args) b2) | CRecord pars -> CRecord (List.map (fun (e,o) -> e, add_args id new_args o) pars) | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.") diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index 24304e361..f209fb19f 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -1,5 +1,5 @@ open Names -open Misctypes +open Tactypes val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index cc92a73f0..439274240 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -23,7 +23,7 @@ open Tacticals open Tactics open Indfun_common open Tacmach -open Misctypes +open Tactypes open Termops open Context.Rel.Declaration @@ -239,7 +239,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i List.map (fun decl -> List.map - (fun id -> CAst.make @@ IntroNaming (IntroIdentifier id)) + (fun id -> CAst.make @@ IntroNaming (Namegen.IntroIdentifier id)) (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl))))) ) branches @@ -257,7 +257,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i List.fold_right (fun {CAst.v=pat} acc -> match pat with - | IntroNaming (IntroIdentifier id) -> id::acc + | IntroNaming (Namegen.IntroIdentifier id) -> id::acc | _ -> anomaly (Pp.str "Not an identifier.") ) (List.nth intro_pats (pred i)) diff --git a/plugins/funind/invfun.mli b/plugins/funind/invfun.mli index 9151fd0e2..3ddc60920 100644 --- a/plugins/funind/invfun.mli +++ b/plugins/funind/invfun.mli @@ -9,7 +9,7 @@ (************************************************************************) val invfun : - Misctypes.quantified_hypothesis -> + Tactypes.quantified_hypothesis -> Names.GlobRef.t option -> Evar.t Evd.sigma -> Evar.t list Evd.sigma val derive_correctness : diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 72bb8253d..aa49148fc 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -37,7 +37,7 @@ open Glob_term open Pretyping open Termops open Constrintern -open Misctypes +open Tactypes open Genredexpr open Equality -- cgit v1.2.3