diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
| commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
| tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /parsing/tacextend.ml4 | |
| parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff) | |
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/tacextend.ml4')
| -rw-r--r-- | parsing/tacextend.ml4 | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index d52ab8dd7..517e34aa2 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -43,7 +43,7 @@ let rec make_let e = function let loc = join_loc loc (MLast.loc_of_expr e) in let e = make_let e l in let v = <:expr< Genarg.out_gen $make_wit loc t$ $lid:p$ >> in - let v = + let v = (* Special case for tactics which must be stored in algebraic form to avoid marshalling closures and to be reprinted *) if is_tactic_genarg t then @@ -95,7 +95,7 @@ let rec make_eval_tactic e = function let rec make_fun e = function | [] -> e - | GramNonTerminal(loc,_,_,Some p)::l -> + | GramNonTerminal(loc,_,_,Some p)::l -> let p = Names.string_of_id p in <:expr< fun $lid:p$ -> $make_fun e l$ >> | _::l -> make_fun e l @@ -138,7 +138,7 @@ let rec contains_epsilon = function | ExtraArgType("hintbases") -> true | _ -> false let is_atomic = function - | GramTerminal s :: l when + | GramTerminal s :: l when List.for_all (function GramTerminal _ -> false | GramNonTerminal(_,t,_,_) -> contains_epsilon t) l @@ -152,7 +152,7 @@ let declare_tactic loc s cl = let hide_tac (p,e) = (* reste a definir les fonctions cachees avec des noms frais *) let stac = "h_"^s in - let e = + let e = make_fun <:expr< Refiner.abstract_extended_tactic $mlexpr_of_string s$ $make_args p$ $make_eval_tactic e p$ @@ -194,7 +194,7 @@ EXTEND ; tacrule: [ [ "["; l = LIST1 tacargs; "]"; "->"; "["; e = Pcaml.expr; "]" - -> + -> if match List.hd l with GramNonTerminal _ -> true | _ -> false then (* En attendant la syntaxe de tacticielles *) failwith "Tactic syntax must start with an identifier"; |