diff options
| author | herbelin | 2002-11-24 23:13:25 +0000 |
|---|---|---|
| committer | herbelin | 2002-11-24 23:13:25 +0000 |
| commit | 5c7cd2b0c85470a96b1edb09956ebef8e5d45cfe (patch) | |
| tree | b531583709303b92d62dee37571250eb7cde48c7 /parsing/ast.ml | |
| parent | d2b7a94fe0ed982a6dd7ff2c07991c2f1b1a6fc8 (diff) | |
Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; améliorations diverses de l'affichage; affinement de la syntaxe et des options de Notation; branchement de Syntactic Definition sur Notation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3270 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/ast.ml')
| -rwxr-xr-x | parsing/ast.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/parsing/ast.ml b/parsing/ast.ml index ae677979ff..13989bcbb5 100755 --- a/parsing/ast.ml +++ b/parsing/ast.ml @@ -345,6 +345,8 @@ let rec amatch alp sigma spat ast = | (Pmeta(pv,Tlist),_) -> grammar_type_error (loc ast,"Ast.amatch") | (Pmeta_slam(pv,pb), Slam(loc, Some s, b)) -> amatch alp (bind_env_ast sigma pv (Nvar(loc,s))) pb b + | (Pmeta_slam(pv,pb), Slam(loc, None, b)) -> + amatch alp (bind_env_ast sigma pv (Nvar(loc,id_of_string "_"))) pb b | (Pmeta_slam(pv,pb), Smetalam(loc, s, b)) -> anomaly "amatch: match a pattern with an open ast" | (Pnode(nodp,argp), Node(loc,op,args)) when nodp = op -> |