diff options
| -rw-r--r-- | CREDITS | 19 | ||||
| -rwxr-xr-x | configure | 4 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 22 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 4 |
4 files changed, 33 insertions, 16 deletions
@@ -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) *************************************************************************** @@ -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 a34873166..d926684b3 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 6f1e95d60..9658f792e 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 |