From c3ca134628ad4d9ef70a13b65c48ff17c737238f Mon Sep 17 00:00:00 2001 From: ppedrot Date: Tue, 18 Dec 2012 18:52:54 +0000 Subject: Modulification of name git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/funind/glob_termops.mli | 47 +++++++++++++++++++++-------------------- 1 file changed, 24 insertions(+), 23 deletions(-) (limited to 'plugins/funind/glob_termops.mli') diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 55d793e03..0f10636f0 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -1,8 +1,9 @@ +open Names open Glob_term open Misctypes (* [get_pattern_id pat] returns a list of all the variable appearing in [pat] *) -val get_pattern_id : cases_pattern -> Names.Id.t list +val get_pattern_id : cases_pattern -> Id.t list (* [pattern_to_term pat] returns a glob_constr corresponding to [pat]. [pat] must not contain occurences of anonymous pattern @@ -14,11 +15,11 @@ val pattern_to_term : cases_pattern -> glob_constr In each of them the location is Util.Loc.ghost *) val mkGRef : Globnames.global_reference -> glob_constr -val mkGVar : Names.Id.t -> glob_constr +val mkGVar : Id.t -> glob_constr val mkGApp : glob_constr*(glob_constr list) -> glob_constr -val mkGLambda : Names.name * glob_constr * glob_constr -> glob_constr -val mkGProd : Names.name * glob_constr * glob_constr -> glob_constr -val mkGLetIn : Names.name * glob_constr * glob_constr -> glob_constr +val mkGLambda : Name.t * glob_constr * glob_constr -> glob_constr +val mkGProd : Name.t * glob_constr * glob_constr -> glob_constr +val mkGLetIn : Name.t * glob_constr * glob_constr -> glob_constr val mkGCases : glob_constr option * tomatch_tuples * cases_clauses -> glob_constr val mkGSort : glob_sort -> glob_constr val mkGHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *) @@ -27,15 +28,15 @@ val mkGCast : glob_constr* glob_constr -> glob_constr Some basic functions to decompose glob_constrs These are analogous to the ones constrs *) -val glob_decompose_prod : glob_constr -> (Names.name*glob_constr) list * glob_constr +val glob_decompose_prod : glob_constr -> (Name.t*glob_constr) list * glob_constr val glob_decompose_prod_or_letin : - glob_constr -> (Names.name*glob_constr option*glob_constr option) list * glob_constr -val glob_decompose_prod_n : int -> glob_constr -> (Names.name*glob_constr) list * glob_constr + glob_constr -> (Name.t*glob_constr option*glob_constr option) list * glob_constr +val glob_decompose_prod_n : int -> glob_constr -> (Name.t*glob_constr) list * glob_constr val glob_decompose_prod_or_letin_n : int -> glob_constr -> - (Names.name*glob_constr option*glob_constr option) list * glob_constr -val glob_compose_prod : glob_constr -> (Names.name*glob_constr) list -> glob_constr + (Name.t*glob_constr option*glob_constr option) list * glob_constr +val glob_compose_prod : glob_constr -> (Name.t*glob_constr) list -> glob_constr val glob_compose_prod_or_letin: glob_constr -> - (Names.name*glob_constr option*glob_constr option) list -> glob_constr + (Name.t*glob_constr option*glob_constr option) list -> glob_constr val glob_decompose_app : glob_constr -> glob_constr*(glob_constr list) @@ -57,7 +58,7 @@ val glob_make_or_list : glob_constr list -> glob_constr (* Replace the var mapped in the glob_constr/context *) -val change_vars : Names.Id.t Names.Id.Map.t -> glob_constr -> glob_constr +val change_vars : Id.t Id.Map.t -> glob_constr -> glob_constr @@ -69,27 +70,27 @@ val change_vars : Names.Id.t Names.Id.Map.t -> glob_constr -> glob_constr [avoid] with the variables appearing in the result. *) val alpha_pat : - Names.Id.Map.key list -> + Id.Map.key list -> Glob_term.cases_pattern -> - Glob_term.cases_pattern * Names.Id.Map.key list * - Names.Id.t Names.Id.Map.t + Glob_term.cases_pattern * Id.Map.key list * + Id.t Id.Map.t (* [alpha_rt avoid rt] alpha convert [rt] s.t. the result repects barendregt conventions and does not share bound variables with avoid *) -val alpha_rt : Names.Id.t list -> glob_constr -> glob_constr +val alpha_rt : Id.t list -> glob_constr -> glob_constr (* same as alpha_rt but for case branches *) -val alpha_br : Names.Id.t list -> - Loc.t * Names.Id.t list * Glob_term.cases_pattern list * +val alpha_br : Id.t list -> + Loc.t * Id.t list * Glob_term.cases_pattern list * Glob_term.glob_constr -> - Loc.t * Names.Id.t list * Glob_term.cases_pattern list * + Loc.t * Id.t list * Glob_term.cases_pattern list * Glob_term.glob_constr (* Reduction function *) val replace_var_by_term : - Names.Id.t -> + Id.t -> Glob_term.glob_constr -> Glob_term.glob_constr -> Glob_term.glob_constr @@ -97,7 +98,7 @@ val replace_var_by_term : (* [is_free_in id rt] checks if [id] is a free variable in [rt] *) -val is_free_in : Names.Id.t -> glob_constr -> bool +val is_free_in : Id.t -> glob_constr -> bool val are_unifiable : cases_pattern -> cases_pattern -> bool @@ -109,10 +110,10 @@ val eq_cases_pattern : cases_pattern -> cases_pattern -> bool ids_of_pat : cases_pattern -> Id.Set.t returns the set of variables appearing in a pattern *) -val ids_of_pat : cases_pattern -> Names.Id.Set.t +val ids_of_pat : cases_pattern -> Id.Set.t (* TODO: finish this function (Fix not treated) *) -val ids_of_glob_constr: glob_constr -> Names.Id.Set.t +val ids_of_glob_constr: glob_constr -> Id.Set.t (* removing let_in construction in a glob_constr -- cgit v1.2.3