aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/tacexpr.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 17961fd42..1808fd3aa 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -96,7 +96,7 @@ type 'id gclause =
{ onhyps : 'id raw_hyp_location list option;
concl_occs : bool * int or_var list }
-let nowhere = {onhyps=Some[]; concl_occs=(false,[])}
+let nowhere = {onhyps=Some[]; concl_occs=no_occurrences_expr}
let simple_clause_of = function
| { onhyps = Some [scl]; concl_occs = occs } when occs = no_occurrences_expr ->