From b96e45b1714c12daa1127e8bf14467eea07ebe17 Mon Sep 17 00:00:00 2001 From: barras Date: Fri, 2 Jan 2004 20:28:44 +0000 Subject: meilleure presentation des commentaires du traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5168 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/g_tactic.ml4 | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'parsing/g_tactic.ml4') diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index cf10f0c45..e05ed48c5 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -32,7 +32,8 @@ let _ = (* Functions overloaded by quotifier *) let induction_arg_of_constr c = - try ElimOnIdent (Topconstr.constr_loc c,coerce_to_id c) with _ -> ElimOnConstr c + try ElimOnIdent (Topconstr.constr_loc c,snd (coerce_to_id c)) + with _ -> ElimOnConstr c let local_compute = [FBeta;FIota;FDeltaBut [];FZeta] @@ -154,7 +155,7 @@ GEXTEND Gram bindings: [ [ c1 = constr; ":="; c2 = constr; bl = LIST0 simple_binding -> ExplicitBindings - ((join_to_constr loc c2,NamedHyp (coerce_to_id c1), c2) :: bl) + ((join_to_constr loc c2,NamedHyp (snd(coerce_to_id c1)), c2) :: bl) | n = natural; ":="; c = constr; bl = LIST0 simple_binding -> ExplicitBindings ((join_to_constr loc c,AnonHyp n, c) :: bl) | c1 = constr; bl = LIST0 constr -> @@ -292,11 +293,11 @@ GEXTEND Gram | IDENT "Cut"; c = constr -> TacCut c | IDENT "Assert"; c = constr -> TacTrueCut (None,c) | IDENT "Assert"; c = constr; ":"; t = constr -> - TacTrueCut (Some (coerce_to_id c),t) + TacTrueCut (Some (snd(coerce_to_id c)),t) | IDENT "Assert"; c = constr; ":="; b = constr -> - TacForward (false,Names.Name (coerce_to_id c),b) + TacForward (false,Names.Name (snd (coerce_to_id c)),b) | IDENT "Pose"; c = constr; ":="; b = constr -> - TacForward (true,Names.Name (coerce_to_id c),b) + TacForward (true,Names.Name (snd(coerce_to_id c)),b) | IDENT "Pose"; b = constr -> TacForward (true,Names.Anonymous,b) | IDENT "Generalize"; lc = LIST1 constr -> TacGeneralize lc | IDENT "Generalize"; IDENT "Dependent"; c = constr -> TacGeneralizeDep c -- cgit v1.2.3