From d33ced344ba377f0a4003102d77f880fda108fd7 Mon Sep 17 00:00:00 2001 From: glondu Date: Fri, 24 Dec 2010 23:49:21 +0000 Subject: More {raw => glob} changes for consistency perl -pi -e 's/(\W|_)raw((?:sort|_prop|terms?|_branch|_red_flag|pat tern|_constr_of|_of_pat)(?:\W|_))/\1glob_\2/g;s/glob__/glob_/g;s/(\ W)R((?:Prop|Type|Fix|CoFix|StructRec|WfRec|MeasureRec)\W)/\1G\2/g;s /glob_terms?/glob_constr/g' **/*.ml* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13756 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/funind/glob_termops.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/funind/glob_termops.mli') diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index b6c407a24..3afb86298 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -23,7 +23,7 @@ val mkRLambda : Names.name * glob_constr * glob_constr -> glob_constr val mkRProd : Names.name * glob_constr * glob_constr -> glob_constr val mkRLetIn : Names.name * glob_constr * glob_constr -> glob_constr val mkRCases : glob_constr option * tomatch_tuples * cases_clauses -> glob_constr -val mkRSort : rawsort -> glob_constr +val mkRSort : glob_sort -> glob_constr val mkRHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *) val mkRCast : glob_constr* glob_constr -> glob_constr (* @@ -115,10 +115,10 @@ val eq_cases_pattern : cases_pattern -> cases_pattern -> bool val ids_of_pat : cases_pattern -> Names.Idset.t (* TODO: finish this function (Fix not treated) *) -val ids_of_rawterm: glob_constr -> Names.Idset.t +val ids_of_glob_constr: glob_constr -> Names.Idset.t (* - removing let_in construction in a rawterm + removing let_in construction in a glob_constr *) val zeta_normalize : Glob_term.glob_constr -> Glob_term.glob_constr -- cgit v1.2.3