diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-27 07:55:30 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-27 07:55:30 +0000 |
| commit | b7a2a4728aae75eba4750b7c3e0dc60c624b76cf (patch) | |
| tree | 8f7d966d3ca70d1318c0912122ab65df368e1462 /parsing/g_tactic.ml4 | |
| parent | 8c6fb6f52db5bfda6cdfeb4f581da1332fb4a20b (diff) | |
Complement to 12347 and 12348 on the extended syntax of case/elim.
Don't change the semantics of "case 1" and forbid the use of numbers
to refer to non-dependent quantified hypotheses in the more general
forms that are synonymous of "destruct" (don't want to commit to a
syntax for non-dependent quantified hypotheses which is ambiguous and
after all not so appealing: for instance, something like destruct @1,
destruct #1, or destruct at 1, or destruct :(ind_pattern), meaning in
the latter case the first hypothesis whose type matches ind_pattern,
would have probably been better).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12355 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_tactic.ml4')
| -rw-r--r-- | parsing/g_tactic.ml4 | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 68e437cab..928aa3e09 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -150,9 +150,21 @@ let induction_arg_of_constr (c,lbind as clbind) = let mkTacCase with_evar = function | [([ElimOnConstr cl],None,(None,None))],None -> TacCase (with_evar,cl) + (* Reinterpret numbers as a notation for terms *) + | [([(ElimOnAnonHyp n)],None,(None,None))],None -> + TacCase (with_evar, + (CPrim (dummy_loc, Numeral (Bigint.of_string (string_of_int n))), + NoBindings)) + (* Reinterpret ident as notations for variables in the context *) + (* because we don't know if they are quantified or not *) | [([ElimOnIdent id],None,(None,None))],None -> TacCase (with_evar,(CRef (Ident id),NoBindings)) | ic -> + if List.exists (fun (cl,a,b) -> + List.exists (function ElimOnAnonHyp _ -> true | _ -> false) cl) + (fst ic) + then + error "Use of numbers as direct arguments of 'case' is not supported."; TacInductionDestruct (false,with_evar,ic) let rec mkCLambdaN_simple_loc loc bll c = |