From 215f42dae466bbbdb865303af05c7e70b5fb3d15 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 21 May 2003 13:11:15 +0000
Subject: Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de
 noms pour les metavariables de patterns; fusion NoHypId et Hyp
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4043 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_constrnew.ml4 | 3 +++
 parsing/g_tacticnew.ml4 | 4 ++--
 parsing/lexer.ml4       | 2 +-
 parsing/pptactic.ml     | 3 +--
 parsing/q_coqast.ml4    | 3 +--
 5 files changed, 8 insertions(+), 7 deletions(-)

(limited to 'parsing')

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
-- 
cgit v1.2.3