diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_type.ml | 2 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 2 | ||||
| -rw-r--r-- | proofs/tacexpr.ml | 7 |
3 files changed, 3 insertions, 8 deletions
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 5bd8060ae1..9f81ffee7f 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -92,8 +92,6 @@ and tactic_arg = glob_tactic_expr) Tacexpr.gen_tactic_arg -type hyp_location = identifier Tacexpr.raw_hyp_location - type ltac_call_kind = | LtacNotationCall of string | LtacNameCall of ltac_constant diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 0bd0eaa113..5fb463da73 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -127,8 +127,6 @@ and tactic_arg = glob_tactic_expr) Tacexpr.gen_tactic_arg -type hyp_location = identifier Tacexpr.raw_hyp_location - type ltac_call_kind = | LtacNotationCall of string | LtacNameCall of ltac_constant diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 2413e73ecf..6b153fa102 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -98,23 +98,22 @@ type 'id message_token = | MsgInt of int | MsgIdent of 'id -type 'id gsimple_clause = ('id raw_hyp_location) option (* onhyps: [None] means *on every hypothesis* [Some l] means on hypothesis belonging to l *) type 'id gclause = { onhyps : 'id raw_hyp_location list option; - concl_occs : bool * int or_var list } + concl_occs : occurrences_expr } let nowhere = {onhyps=Some[]; concl_occs=no_occurrences_expr} -let simple_clause_of = function +let goal_location_of = function | { onhyps = Some [scl]; concl_occs = occs } when occs = no_occurrences_expr -> Some scl | { onhyps = Some []; concl_occs = occs } when occs = all_occurrences_expr -> None | _ -> - error "not a simple clause (one hypothesis or conclusion)" + error "Not a simple \"in\" clause (one hypothesis or the conclusion)" type ('constr,'id) induction_clause = ('constr with_bindings induction_arg list * 'constr with_bindings option * |