diff options
| author | herbelin | 2002-12-15 12:12:49 +0000 |
|---|---|---|
| committer | herbelin | 2002-12-15 12:12:49 +0000 |
| commit | 6c0bd550e1cc40443ac3d42b68dd5c098afbba4f (patch) | |
| tree | 5fa9820daf2256e6963e0455bc13fab83a8235ba /interp/constrintern.mli | |
| parent | d618791e00b0550b8e639bd63df451c2ab13805a (diff) | |
Prise en compte des scopes traversés dans les notations
Traitement spécial pour le scope type_scope à l'internalisation
Ajout "Locate Notation"
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3441 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 8666db6338..4c185a788e 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -36,7 +36,7 @@ type implicits_env = (identifier * Impargs.implicits_list) list (* Interprets global names, including syntactic defs and section variables *) val interp_rawconstr : evar_map -> env -> constr_expr -> rawconstr -val interp_rawconstr_gen : evar_map -> env -> implicits_env -> +val interp_rawconstr_gen : bool -> evar_map -> env -> implicits_env -> bool -> identifier list -> constr_expr -> rawconstr (*s Composing the translation with typing *) @@ -83,7 +83,7 @@ val interp_constrpattern : val interp_reference : identifier list -> reference -> rawconstr (* Interprets into a abbreviatable constr *) -val interp_aconstr : constr_expr -> aconstr +val interp_aconstr : identifier list -> constr_expr -> interpretation (* Globalization leak for Grammar *) val for_grammar : ('a -> 'b) -> 'a -> 'b |