diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-13 13:09:41 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-13 13:09:41 +0000 |
| commit | 3690735581c7995e4be17c3a3029e66ddf2d3e49 (patch) | |
| tree | 68dde8eac50aa60d99cbe93cf1679af55edc8dea /parsing/ast.mli | |
| parent | 6272fe2c65ccace5982515ec58398505a22855dc (diff) | |
Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; hack temporaire autour du printer
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3120 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/ast.mli')
| -rwxr-xr-x | parsing/ast.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/ast.mli b/parsing/ast.mli index 07dbd06f2..9fd8e9cc9 100755 --- a/parsing/ast.mli +++ b/parsing/ast.mli @@ -103,7 +103,7 @@ val coerce_to_id : Coqast.t -> identifier val coerce_qualid_to_id : qualid Util.located -> identifier -val coerce_reference_to_id : Tacexpr.reference_expr -> identifier +val coerce_reference_to_id : reference_expr -> identifier val abstract_binders_ast : Coqast.loc -> string -> Coqast.t -> Coqast.t -> Coqast.t @@ -144,7 +144,7 @@ val replace_vars_ast : (identifier * identifier) list -> Coqast.t -> Coqast.t val bind_env : env -> string -> typed_ast -> env val ast_match : env -> astpat -> Coqast.t -> env val astl_match : env -> patlist -> Coqast.t list -> env -val first_match : ('a -> astpat) -> env -> t -> 'a list -> ('a * env) option +val find_all_matches : ('a -> astpat) -> env -> t -> 'a list -> ('a * env) list val first_matchl : ('a -> patlist) -> env -> Coqast.t list -> 'a list -> ('a * env) option |