Backport from v8.2 branch of 11986 (interpretation of quantified

hypotheses in induction, unbalanced parenthesis in ltac call stack
printer) and 12003 (late update of CREDITS) + update of magic numbers
(using a somehow arbitrary value between the 8.2 magic numbers and the
possibly forthcoming 8.3 magic numbers).



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

4 files changed, 33 insertions, 16 deletions

diff --git a/CREDITS b/CREDITS
index c982d6724a..3587eec59b 100644
--- a/CREDITS
+++ b/CREDITS
@@ -50,8 +50,6 @@ plugins/interface
   at Nijmegen, 2007-2008)
 plugins/omega
   developed by Pierre Crégut (France Telecom R&D, 1996)
-plugins/recdef
-  developed by Yves Bertot (INRIA-Marelle, 2005-2006)
 plugins/ring
   developed by Samuel Boutin (INRIA-Coq, 1996) and Patrick 
   Loiseleur (LRI, 1997-1999)
@@ -80,16 +78,21 @@ theories/ZArith
   started by Pierre Crégut (France Telecom R&D, 1996)
 theories/IntMap
   developed by Jean Goubault-Larrecq (Dyade, 1998)
+theories/Numbers/Cyclic
+  developed by Benjamin Grégoire (INRIA-Everest, 2007), Laurent Théry
+  (INRIA-Marelle, 2007-2008), Arnaud Spiwack (INRIA-LogiCal, 2007) and
+  Pierre Letouzey (PPS-Paris 7, 2008)
 theories/Strings
   developed by Laurent Théry (INRIA-Lemme, 2003)
 ide/utils
   some files come from Maxence Guesdon's Cameleon tool 
 
-Many discussions within the Démons team at LRI and the LogiCal project
-influenced significantly the design of Coq especially with
+Many discussions within the Démons team at LRI, and the
+LogiCal/TypiCal projects influenced significantly the design of
+components of Coq, especially with
 
-  J. Courant, P. Courtieu, J. Duprat, J. Goubault,
-  A. Miquel, C. Marché, B. Monate, B. Werner.
+  F. Blanqui, J. Courant, P. Courtieu, J. Duprat, S. Glondu, J. Goubault,
+  A. Mahboubi, C. Marché, A. Miquel, B. Monate, P.-Y. Strub, B. Werner.
 
 Intensive users suggested improvements of the system : 
 
@@ -135,9 +138,11 @@ of the Coq Proof assistant during the indicated time :
                             LRI, 1997-now)
   Clément Renard (INRIA, 2001-2004)
   Claudio Sacerdoti Coen (INRIA, 2004-2005)
+  Amokrane Saïbi (INRIA, 1993-1998)
+  Vincent Siles (INRIA, 2007)
+  Élie Soubiran (INRIA, 2007-now)
   Matthieu Sozeau (INRIA, 2005-now)
   Arnaud Spiwack (INRIA, 2006-now)
-  Amokrane Saïbi (INRIA, 1993-1998)
   Benjamin Werner (INRIA, 1989-1994)
 
 ***************************************************************************
diff --git a/configure b/configure
index 1e9dc472f2..7b39eb4229 100755
--- a/configure
+++ b/configure
@@ -7,8 +7,8 @@
 ##################################
 
 VERSION=trunk
-VOMAGIC=08193 
-STATEMAGIC=19764
+VOMAGIC=08211
+STATEMAGIC=58211
 DATE=`LANG=C date +"%B %Y"`
 
 # Create the bin/ directory if non-existent
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a348731660..d926684b31 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -542,7 +542,9 @@ let intern_induction_arg ist = function
   | ElimOnIdent (loc,id) ->
       if !strict_check then
 	(* If in a defined tactic, no intros-until *)
-	ElimOnConstr (intern_constr ist (CRef (Ident (dloc,id))),NoBindings)
+	match intern_constr ist (CRef (Ident (dloc,id))) with
+	| RVar (loc,id),_ -> ElimOnIdent (loc,id)
+	| c -> ElimOnConstr (c,NoBindings)
       else
 	ElimOnIdent (loc,id)
 
@@ -1722,10 +1724,20 @@ let interp_induction_arg ist gl = function
   | ElimOnConstr c -> ElimOnConstr (interp_constr_with_bindings ist gl c)
   | ElimOnAnonHyp n as x -> x
   | ElimOnIdent (loc,id) ->
-      if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id)
-      else ElimOnConstr
-	(pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id)))),
-	 NoBindings)
+      try
+	match List.assoc id ist.lfun with
+	| VInteger n -> ElimOnAnonHyp n
+	| VIntroPattern (IntroIdentifier id) -> ElimOnIdent (loc,id)
+	| VConstr c -> ElimOnConstr (c,NoBindings)
+	| _ -> user_err_loc (loc,"",
+	      strbrk "Cannot coerce " ++ pr_id id ++
+	      strbrk " neither to a quantified hypothesis nor to a term.")
+      with Not_found ->
+	(* Interactive mode *)
+	if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id)
+	else ElimOnConstr
+	  (pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id)))),
+	  NoBindings)
 
 let mk_constr_value ist gl c = VConstr (pf_interp_constr ist gl c)
 let mk_hyp_value ist gl c = VConstr (mkVar (interp_hyp ist gl c))
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 6f1e95d603..9658f792e8 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -822,8 +822,8 @@ let explain_ltac_call_trace (nrep,last,trace,loc) =
 		  prlist_with_sep pr_coma
 		  (fun (id,c) -> 
 		     pr_id id ++ str ":=" ++ Printer.pr_lconstr c)
-		  (List.rev vars @ unboundvars)
-	      else mt()) ++ str ")") ++
+		  (List.rev vars @ unboundvars) ++ str ")"
+	      else mt())) ++
       (if n=2 then str " (repeated twice)"
        else if n>2 then str " (repeated "++int n++str" times)"
        else mt()) in