diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-24 23:49:21 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-24 23:49:21 +0000 |
| commit | d33ced344ba377f0a4003102d77f880fda108fd7 (patch) | |
| tree | a8f7642bb599a08ada8b6392d0fa14f823e57e3c /plugins/funind/glob_termops.mli | |
| parent | 6ebd4c4ad28d46965623e72d8654c36fcc6fe9b0 (diff) | |
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
Diffstat (limited to 'plugins/funind/glob_termops.mli')
| -rw-r--r-- | plugins/funind/glob_termops.mli | 6 |
1 files changed, 3 insertions, 3 deletions
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 |