diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-01 14:45:20 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-01 14:45:20 +0000 |
| commit | 124016815a5a38dfebee75451721ae13bca81959 (patch) | |
| tree | b3adc59b7ecc5fb6093e21a741bf764fa206864f /parsing | |
| parent | 97fb9f22eadab06fe320ccedf6abfb6be89702f4 (diff) | |
Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient
pas correctes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10739 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_intsyntax.ml | 2 | ||||
| -rw-r--r-- | parsing/g_rsyntax.ml | 2 | ||||
| -rw-r--r-- | parsing/g_string_syntax.ml | 2 | ||||
| -rw-r--r-- | parsing/g_tactic.ml4 | 8 | ||||
| -rw-r--r-- | parsing/q_constr.ml4 | 2 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 4 |
6 files changed, 14 insertions, 6 deletions
diff --git a/parsing/g_intsyntax.ml b/parsing/g_intsyntax.ml index b1a8ae348..4528fde9c 100644 --- a/parsing/g_intsyntax.ml +++ b/parsing/g_intsyntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $ $ i*) +(*i $Id:$ i*) (* digit-based syntax for int31, bigN bigZ and bigQ *) diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml index 456479038..3218781d1 100644 --- a/parsing/g_rsyntax.ml +++ b/parsing/g_rsyntax.ml @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i $Id:$ i*) + open Pp open Util open Names diff --git a/parsing/g_string_syntax.ml b/parsing/g_string_syntax.ml index 6d879fb20..6b1faa76c 100644 --- a/parsing/g_string_syntax.ml +++ b/parsing/g_string_syntax.ml @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) +(*i $Id:$ i*) + open Pp open Util open Names diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index b076220b4..64062765a 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -365,8 +365,12 @@ GEXTEND Gram | IDENT "exact_no_check"; c = constr -> TacExactNoCheck c | IDENT "vm_cast_no_check"; c = constr -> TacVmCastNoCheck c - | IDENT "apply"; cl = constr_with_bindings -> TacApply (false,cl) - | IDENT "eapply"; cl = constr_with_bindings -> TacApply (true,cl) + | IDENT "apply"; cl = constr_with_bindings -> TacApply (true,false,cl) + | IDENT "eapply"; cl = constr_with_bindings -> TacApply (true,true,cl) + | IDENT "simple"; IDENT "apply"; cl = constr_with_bindings -> + TacApply (false,false,cl) + | IDENT "simple"; IDENT "eapply"; cl = constr_with_bindings -> + TacApply (false, true,cl) | IDENT "elim"; cl = constr_with_bindings; el = OPT eliminator -> TacElim (false,cl,el) | IDENT "eelim"; cl = constr_with_bindings; el = OPT eliminator -> diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 index 497b8a3c6..44ca8eb2c 100644 --- a/parsing/q_constr.ml4 +++ b/parsing/q_constr.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) -(* $Id: g_constr.ml4,v 1.58 2005/12/30 10:55:32 herbelin Exp $ *) +(* $Id$ *) open Rawterm open Term diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 922c7af16..55b531585 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -295,8 +295,8 @@ let rec mlexpr_of_atomic_tactic = function <:expr< Tacexpr.TacExactNoCheck $mlexpr_of_constr c$ >> | Tacexpr.TacVmCastNoCheck c -> <:expr< Tacexpr.TacVmCastNoCheck $mlexpr_of_constr c$ >> - | Tacexpr.TacApply (false,cb) -> - <:expr< Tacexpr.TacApply False $mlexpr_of_constr_with_binding cb$ >> + | Tacexpr.TacApply (b,false,cb) -> + <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_constr_with_binding cb$ >> | Tacexpr.TacElim (false,cb,cbo) -> let cb = mlexpr_of_constr_with_binding cb in let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in |