diff options
author | 2010-12-23 18:50:45 +0000 | |
---|---|---|
committer | 2010-12-23 18:50:45 +0000 | |
commit | 8f9461509338a3ebba46faaad3116c4e44135423 (patch) | |
tree | 23da64d38f2194a1f9e42b789b16b82402d6908f /proofs/goal.mli | |
parent | fafba6b545c7d0d774bcd79bdbddb8869517aabb (diff) |
Change of nomenclature: rawconstr -> glob_constr
There was a discrepancy of the notions "raw" and "globalized" between
constrs and tactics, and some confusion of the notions in
e.g. genarg.mli (see all globwit_* there). This commit is a first step
towards unification of terminology between constrs and
tactics. Changes in module names will be done separately.
In extraargs.ml4, the "ARGUMENT EXTEND raw" and related stuff, even
affected by this change, has not been touched and highlights another
confusion in "ARGUMENT EXTEND" in general that will be addressed
later.
The funind plugin doesn't respect the same naming conventions as the
rest, so leave some "raw" there for now... they will be addressed
later.
This big commit has been generated with the following command (wrapped
here, but should be on a *single* line):
perl -pi -e 's/(\W(?:|pp|pr_l)|_)raw((?:constrs?|type|vars|_binder|
_context|decl|_decompose|_compose|_make)(?:\W|_))/\1glob_\2/g;s/glo
b__/glob_/g;s/prraw/prglob/g;s/(\W)R((?:Ref|Var|Evar|PatVar|App|Lam
bda|Prod|LetIn|Cases|LetTuple|If|Rec|Sort|Hole|Cast|Dynamic)\W)/\1G
\2/g' `git ls-files|grep -v dev/doc/changes.txt`
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13743 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/goal.mli')
-rw-r--r-- | proofs/goal.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/goal.mli b/proofs/goal.mli index b291e1a77..3d9fcc5a2 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -69,11 +69,11 @@ module Refinable : sig The [check_type] argument asks whether the term should have the same type as the conclusion. [resolve_classes] is a flag on pretyping functions which, if set to true, calls the typeclass resolver. - The principal argument is a [rawconstr] which is then pretyped in the + The principal argument is a [glob_constr] which is then pretyped in the context of a term, the remaining evars are registered to the handle. It is the main component of the toplevel refine tactic.*) val constr_of_raw : - handle -> bool -> bool -> Rawterm.rawconstr -> Term.constr sensitive + handle -> bool -> bool -> Rawterm.glob_constr -> Term.constr sensitive end |