Diverses corrections

- gestion des idents (suite commit 10785) [lib, interp, contrib/ring, dev]
- suppression (enfin) des $id dans les constr (utilisation des MetaIdArg des
  quotations de tactiques pour simuler les métas des constr - quitte à devoir
  utiliser un let-in dans l'expression de tactique) [proofs, parsing, tactics]
- utilisation de error en place d'un "print_string" d'échec dans fourier
- améliorations espérées vis à vis de quelques "bizarreries" dans la gestion
  des Meta [pretyping]



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

2 files changed, 6 insertions, 4 deletions

diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml
index d415cf7d24..ef0ff426dc 100644
--- a/contrib/fourier/fourierR.ml
+++ b/contrib/fourier/fourierR.ml
@@ -503,8 +503,7 @@ let rec fourier gl=
     let res=fourier_lineq (!lineq) in
     let tac=ref tclIDTAC in
     if res=[]
-    then (print_string "Tactic Fourier fails.\n";
-		       flush stdout)
+    then Util.error "fourier failed"
     (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
     else (match res with
         [(cres,sres,lc)]->
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index 3c1645d477..3b13283e13 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -191,8 +191,11 @@ let decomp_term c = kind_of_term (strip_outer_cast c)
   ?2 ?1)}, where \texttt{C} is the [i]-th constructor of inductive
   type [typ] *)
 
-let coerce_meta_out id = int_of_string (string_of_id id)
-let coerce_meta_in n = id_of_string (string_of_int n)
+let coerce_meta_out id = 
+  let s = string_of_id id in
+  int_of_string (String.sub s 1 (String.length s - 1))
+let coerce_meta_in n =
+  id_of_string ("M" ^ string_of_int n)
 
 let compute_lhs typ i nargsi =
   match kind_of_term typ with