diff options
| author | herbelin | 2004-01-13 15:22:04 +0000 |
|---|---|---|
| committer | herbelin | 2004-01-13 15:22:04 +0000 |
| commit | 0ea28e6a440e39f9f9645aa55afbfa38a0560b27 (patch) | |
| tree | 0c211363f17f8b61de400d1cf65ffd88e33cbaea /parsing | |
| parent | 04d270a46e8c481e0b1f21904c6b25f0b7359fa0 (diff) | |
Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables a b:A' et 'Variables (a:A) (b:A)'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5198 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 11 | ||||
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 11 |
2 files changed, 7 insertions, 15 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b1e6cda093..d79b3ec3a8 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -20,9 +20,6 @@ open Vernac_ open Prim open Decl_kinds -(* Dans join_binders, s'il y a un "?", on perd l'info qu'il est partagé *) -let join_binders (idl,c) = List.map (fun id -> (id,c)) idl - open Genarg let evar_constr loc = CHole loc @@ -94,7 +91,7 @@ GEXTEND Gram END let test_plurial_form = function - | [_] -> + | [_,([_],_)] -> Options.if_verbose warning "Keywords Variables/Hypotheses/Parameters expect more than one assumption" | _ -> () @@ -135,12 +132,12 @@ GEXTEND Gram | ":" -> false ] ] ; params: - [ [ idl = LIST1 identref SEP ","; coe = of_type_with_opt_coercion; c = constr - -> List.map (fun c -> (coe,c)) (join_binders (idl,c)) + [ [ idl = LIST1 identref SEP ","; coe = of_type_with_opt_coercion; + c = constr -> (coe,(idl,c)) ] ] ; ne_params_list: - [ [ ll = LIST1 params SEP ";" -> List.flatten ll ] ] + [ [ ll = LIST1 params SEP ";" -> ll ] ] ; name_comma_list_tail: [ [ ","; nal = LIST1 name SEP "," -> nal | -> [] ] ] diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index 8142303043..8808ef0258 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -86,10 +86,6 @@ let no_coercion loc (c,x) = (loc,"no_coercion",Pp.str"no coercion allowed here"); x -let flatten_assum l = - List.flatten - (List.map (fun (oc,(idl,t)) -> List.map (fun id -> (oc,(id,t))) idl) l) - (* Gallina declarations *) if not !Options.v7 then GEXTEND Gram @@ -104,11 +100,10 @@ GEXTEND Gram | (f,d) = def_token; id = identref; b = def_body -> VernacDefinition (d, id, b, f) | stre = assumption_token; bl = assum_list -> - VernacAssumption (stre, flatten_assum bl) + VernacAssumption (stre, bl) | stre = assumptions_token; bl = assum_list -> - let l = flatten_assum bl in - test_plurial_form l; - VernacAssumption (stre, l) + test_plurial_form bl; + VernacAssumption (stre, bl) (* Gallina inductive declarations *) | f = finite_token; indl = LIST1 inductive_definition SEP "with" -> |