diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-11 10:55:32 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-11 10:55:32 +0000 |
commit | 8659ff43db85c43df644da6ac08509374aabcad4 (patch) | |
tree | 83b7e6318a45245bac501f14c4ea01dfc7b99e3a /interp/constrintern.mli | |
parent | dbd84fb57142a15b11a2ead23ed651ae8b2382a8 (diff) |
Improving abbreviations/notations + backtrack of semantic change in r12439
- Deactivation of short names registration and printing for
abbreviations to identical names, what avoids printing uselessly
qualified names binding where the short name is in fact equivalent.
- New treatment of abbreviations to names: don't insert any maximally
inserted implicit arguments at all at the time of the abbreviation
and use the regular internalization strategy to have them inserted
at use time.
- The previous modifications altogether make redirections of
qualified names easier and avoid the semantic change of r12349 and
hence allows to keep "Notation b := @a" as it was before, i.e. as a
notation for the deactivation of the implicit arguments of a.
- Took benefit of these changes and updated nil/cons/list/app
redefinition in "List.v".
- Fixed parsing/printing notation bugs (loop on partially applied
abreviations for constructors in constrintern.ml + bad reverting of
notations with holes that captured non anonymous variables in
match_cases_pattern).
- Add support for parsing/printing abbreviations to @-like constructors
and for reverting printing for abbreviations to constructors applied
to parameters only (function extern_symbol_pattern).
- Minor error messages fixes and minor APIs cleaning.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12494 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrintern.mli')
-rw-r--r-- | interp/constrintern.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index b08b8dd1f..ee677e80a 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -144,6 +144,10 @@ val intern_constr_pattern : evar_map -> env -> ?as_type:bool -> ?ltacvars:ltac_sign -> constr_pattern_expr -> patvar list * constr_pattern +(* Raise Not_found if syndef not bound to a name and error if unexisting ref *) +val intern_reference : reference -> global_reference + +(* Expands abbreviations (syndef); raise an error if not existing *) val interp_reference : ltac_sign -> reference -> rawconstr (* Interpret binders *) @@ -161,8 +165,8 @@ val interp_context_evars : ?fail_anonymous:bool -> evar_defs ref -> env -> local_binder list -> (env * rel_context) * manual_implicits (* Locating references of constructions, possibly via a syntactic definition *) +(* (these functions do not modify the glob file) *) -val locate_reference : qualid -> global_reference val is_global : identifier -> bool val construct_reference : named_context -> identifier -> constr val global_reference : identifier -> constr |