From 5eae5b130f87aabdfee23bbc9f4114fb5c0624b1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 14 Apr 2008 22:34:19 +0000
Subject: 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
---
 proofs/tacexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 7a90040e5e..ca25c722c9 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -241,7 +241,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast =
 and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg =
   | TacDynamic     of loc * Dyn.t
   | TacVoid
-  | MetaIdArg      of loc * string
+  | MetaIdArg      of loc * bool * string
   | ConstrMayEval  of ('constr,'cst) may_eval
   | IntroPattern   of intro_pattern_expr
   | Reference      of 'ref
-- 
cgit v1.2.3