diff options
| author | herbelin | 2003-11-09 15:16:46 +0000 |
|---|---|---|
| committer | herbelin | 2003-11-09 15:16:46 +0000 |
| commit | 49356f9dd870d7d42e1e4ffbfc00906832197ef1 (patch) | |
| tree | 90447c5b975cb581af7284b45cf952d0483ac2f1 /parsing | |
| parent | fc403f2f912cfceef5ff96af379b6e9d912f0c03 (diff) | |
Traduction semantique des InHyp de clause en InHypValue si local def
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4841 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 5 | ||||
| -rw-r--r-- | parsing/g_tacticnew.ml4 | 6 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 5 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 5 |
4 files changed, 13 insertions, 8 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 74352c0bb2..491fd467f7 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -217,8 +217,9 @@ GEXTEND Gram | s = IDENT; c = constr -> ExtraRedExpr (s,c) ] ] ; hypident: - [ [ id = id_or_meta -> InHyp id - | "("; "Type"; "of"; id = id_or_meta; ")" -> InHypType id ] ] + [ [ id = id_or_meta -> id,(InHyp,ref None) + | "("; "Type"; "of"; id = id_or_meta; ")" -> id,(InHypTypeOnly,ref None) + ] ] ; clause: [ [ "in"; idl = LIST1 hypident -> idl diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4 index 45253cd908..29dc5cfba7 100644 --- a/parsing/g_tacticnew.ml4 +++ b/parsing/g_tacticnew.ml4 @@ -268,8 +268,10 @@ GEXTEND Gram | s = IDENT; c = constr -> ExtraRedExpr (s,c) ] ] ; hypident: - [ [ id = id_or_meta -> InHyp id - | "("; IDENT "type"; "of"; id = id_or_meta; ")" -> InHypType id ] ] + [ [ id = id_or_meta -> id,(InHyp,ref None) + | "("; IDENT "type"; "of"; id = id_or_meta; ")" -> id,(InHypTypeOnly,ref None) + | "("; IDENT "value"; "of"; id = id_or_meta; ")" -> id,(InHypValueOnly,ref None) + ] ] ; clause: [ [ "in"; idl = LIST1 hypident -> idl diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 8f0a29c64a..ea5ad236e7 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -136,8 +136,9 @@ let pr_with_names = function | ids -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_case_intro_pattern ids) let pr_hyp_location pr_id = function - | InHyp id -> spc () ++ pr_id id - | InHypType id -> spc () ++ str "(Type of " ++ pr_id id ++ str ")" + | id, (InHyp,_) -> spc () ++ pr_id id + | id, (InHypTypeOnly,_) -> spc () ++ str "(Type of " ++ pr_id id ++ str ")" + | id, _ -> error "Unsupported hyp location in v7" let pr_clause pr_id = function | [] -> mt () diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 7dd14d87a9..01be09fc68 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -159,8 +159,9 @@ let mlexpr_of_loc loc = <:expr< $dloc$ >> let mlexpr_of_hyp = mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident) let mlexpr_of_hyp_location = function - | Tacexpr.InHyp id -> <:expr< Tacexpr.InHyp $mlexpr_of_hyp id$ >> - | Tacexpr.InHypType id -> <:expr< Tacexpr.InHypType $mlexpr_of_hyp id$ >> + | id, (Tacexpr.InHyp,_) -> <:expr< ($mlexpr_of_hyp id$, (Tacexpr.InHyp, ref None)) >> + | id, (Tacexpr.InHypTypeOnly,_) -> <:expr< ($mlexpr_of_hyp id$, (Tacexpr.InHypTypeOnly, ref None)) >> + | id, (Tacexpr.InHypValueOnly,_) -> <:expr< ($mlexpr_of_hyp id$, (Tacexpr.InHypValueOnly,ref None)) >> (* let mlexpr_of_red_mode = function |