diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-02 20:28:44 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-02 20:28:44 +0000 |
| commit | b96e45b1714c12daa1127e8bf14467eea07ebe17 (patch) | |
| tree | 8e5915dc3d72d498495e49a8bbbd7c066cb71026 /parsing/g_tactic.ml4 | |
| parent | 0d3a3d5650cd374eed4272a0de1e3f926a8d3c40 (diff) | |
meilleure presentation des commentaires du traducteur
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5168 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_tactic.ml4')
| -rw-r--r-- | parsing/g_tactic.ml4 | 11 |
1 files changed, 6 insertions, 5 deletions
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 |