diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 97a56cabe6..aadd045478 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -806,7 +806,7 @@ let is_rec_pos (main_ind,wft) = None -> false | Some index -> match fst (Rtree.dest_node wft) with - Mrec i when i = index -> true + Mrec (_,i) when i = index -> true | _ -> false let rec constr_trees (main_ind,wft) ind = |