Autour du parsing:

- Utilisation de notations de type "abbreviation paramétrée" plutôt que
  de notations introduisant des mots-clés, là où c'est possible (cela affecte
  QDen, in_left/in_right, inhabited, S/P dans NZCyclic).
- Extension du lexeur pour qu'il prenne le plus long token valide au
  lieu d'échouer sur un plus long préfixe non valide de token (permet
  notamment de faire passer la notation de Georges "'C_ G ( A )"
  sans invalider toute séquence commençant par 'C et non suivie de _)
- Rajout d'un point final à certains messages d'erreur qui n'en avaient pas.
- Ajout String.copy dans string_of_label ("trou" de mutabilité signalé
  par Georges -- le "trou" lié aux vecteurs des noeuds App restant lui
  ouvert).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11225 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 6 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d2c2b0d6a8..6fc65e9fb7 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -50,7 +50,7 @@ let for_grammar f x =
 type internalisation_error =
   | VariableCapture of identifier
   | WrongExplicitImplicit
-  | NegativeMetavariable
+  | IllegalMetavariable
   | NotAConstructor of reference
   | UnboundFixName of bool * identifier
   | NonLinearPattern of identifier
@@ -66,8 +66,8 @@ let explain_wrong_explicit_implicit =
   str "Found an explicitly given implicit argument but was expecting" ++
   fnl () ++ str "a regular one"
 
-let explain_negative_metavariable =
-  str "Metavariable numbers must be positive"
+let explain_illegal_metavariable =
+  str "Metavariables allowed only in patterns"
 
 let explain_not_a_constructor ref =
   str "Unknown constructor: " ++ pr_reference ref
@@ -102,7 +102,7 @@ let explain_bad_explicitation_number n po =
 let explain_internalisation_error = function
   | VariableCapture id -> explain_variable_capture id
   | WrongExplicitImplicit -> explain_wrong_explicit_implicit
-  | NegativeMetavariable -> explain_negative_metavariable
+  | IllegalMetavariable -> explain_illegal_metavariable
   | NotAConstructor ref -> explain_not_a_constructor ref
   | UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id
   | NonLinearPattern id -> explain_non_linear_pattern id
@@ -940,7 +940,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
     | CPatVar (loc, n) when allow_patvar ->
 	RPatVar (loc, n)
     | CPatVar (loc, _) ->
-	raise (InternalisationError (loc,NegativeMetavariable))
+	raise (InternalisationError (loc,IllegalMetavariable))
     | CEvar (loc, n, l) ->
 	REvar (loc, n, Option.map (List.map (intern env)) l)
     | CSort (loc, s) ->
@@ -1093,7 +1093,8 @@ let internalise sigma globalenv env allow_patvar lvar c =
     intern env c
   with
       InternalisationError (loc,e) ->
-	user_err_loc (loc,"internalize",explain_internalisation_error e)
+	user_err_loc (loc,"internalize",
+	  explain_internalisation_error e ++ str ".")
 
 (**************************************************************************)
 (* Functions to translate constr_expr into rawconstr                       *)