diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-21 13:11:15 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-21 13:11:15 +0000 |
| commit | 215f42dae466bbbdb865303af05c7e70b5fb3d15 (patch) | |
| tree | ef7e2c13c82149b6717e67626af19d3e39c606d5 /parsing | |
| parent | 2e3b255c13bae814715dbdee1fea80f107920cee (diff) | |
Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour les metavariables de patterns; fusion NoHypId et Hyp
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4043 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constrnew.ml4 | 3 | ||||
| -rw-r--r-- | parsing/g_tacticnew.ml4 | 4 | ||||
| -rw-r--r-- | parsing/lexer.ml4 | 2 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 3 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 3 |
5 files changed, 8 insertions, 7 deletions
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4 index a0bd0fb5e..88d108fdd 100644 --- a/parsing/g_constrnew.ml4 +++ b/parsing/g_constrnew.ml4 @@ -179,7 +179,10 @@ GEXTEND Gram | s=sort -> CSort(loc,s) | n=INT -> CNumeral (loc,Bignat.POS (Bignat.of_string n)) | IDENT "_" -> CHole loc +(* | "?"; n=Prim.natural -> CPatVar(loc,(false,Pattern.patvar_of_int n)) ] ] +*) + | "?"; id=ident -> CPatVar(loc,(false,id)) ] ] ; fix_constr: [ [ kw=fix_kw; dcl=fix_decl -> diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4 index fb6e213a4..b299a3368 100644 --- a/parsing/g_tacticnew.ml4 +++ b/parsing/g_tacticnew.ml4 @@ -98,12 +98,12 @@ GEXTEND Gram (* Either an hypothesis or a ltac ref (variable or pattern patvar) *) id_or_ltac_ref: [ [ id = base_ident -> AN id - | "?"; n = natural -> MetaNum (loc,Pattern.patvar_of_int n) ] ] +(* | "?"; n = natural -> MetaNum (loc,Pattern.patvar_of_int n) *) ] ] ; (* Either a global ref or a ltac ref (variable or pattern patvar) *) global_or_ltac_ref: [ [ qid = global -> AN qid - | "?"; n = natural -> MetaNum (loc,Pattern.patvar_of_int n) ] ] +(* | "?"; n = natural -> MetaNum (loc,Pattern.patvar_of_int n) *) ] ] ; (* An identifier or a quotation meta-variable *) id_or_meta: diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 773f97c66..5e27f9ca8 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -307,7 +307,7 @@ let parse_226_tail tk = parser TokIdent (get_buff len) -(* Parse what foolows a dot *) +(* Parse what follows a dot *) let parse_after_dot bp c strm = if !Options.v7 then match strm with parser diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 8e6d63c2d..0f26e390b 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -183,8 +183,7 @@ let pr_match_pattern pr_pat = function | Subterm (Some id,a) -> pr_id id ++ str "[" ++ pr_pat a ++ str "]" let pr_match_hyps pr_pat = function - | NoHypId mp -> str "_:" ++ pr_match_pattern pr_pat mp - | Hyp ((_,id),mp) -> pr_id id ++ str ":" ++ pr_match_pattern pr_pat mp + | Hyp ((_,na),mp) -> pr_name na ++ str ":" ++ pr_match_pattern pr_pat mp let pr_match_rule m pr_pat pr = function | Pat ([],mp,t) when m -> diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 495e2eaff..bb0164962 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -305,9 +305,8 @@ let mlexpr_of_match_pattern = function <:expr< Tacexpr.Subterm $mlexpr_of_option mlexpr_of_ident ido$ $mlexpr_of_pattern_ast t$ >> let mlexpr_of_match_context_hyps = function - | Tacexpr.NoHypId l -> <:expr< Tacexpr.NoHypId $mlexpr_of_match_pattern l$ >> | Tacexpr.Hyp (id,l) -> - let f = mlexpr_of_located mlexpr_of_ident in + let f = mlexpr_of_located mlexpr_of_name in <:expr< Tacexpr.Hyp $f id$ $mlexpr_of_match_pattern l$ >> let mlexpr_of_match_rule f = function |