diff options
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 55 |
1 files changed, 27 insertions, 28 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 51eee2a053..ec0876110b 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -352,35 +352,35 @@ let find_elim hdcncl lft2rgt dep cls ot = (is_global_exists "core.JMeq.type" hdcncl && jmeq_same_dom env sigma ot)) && not dep then - let c = + let c = match EConstr.kind sigma hdcncl with - | Ind (ind_sp,u) -> - let pr1 = + | Ind (ind_sp,u) -> + let pr1 = lookup_eliminator env ind_sp (elimination_sort_of_clause cls gl) - in + in begin match lft2rgt, cls with | Some true, None | Some false, Some _ -> - let c1 = destConstRef pr1 in + let c1 = destConstRef pr1 in let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical c1)) in - let l' = Label.of_id (add_suffix (Label.to_id l) "_r") in + let l' = Label.of_id (add_suffix (Label.to_id l) "_r") in let c1' = Global.constant_of_delta_kn (KerName.make mp l') in - begin - try - let _ = Global.lookup_constant c1' in - c1' - with Not_found -> + begin + try + let _ = Global.lookup_constant c1' in + c1' + with Not_found -> user_err ~hdr:"Equality.find_elim" (str "Cannot find rewrite principle " ++ Label.print l' ++ str ".") end - | _ -> destConstRef pr1 + | _ -> destConstRef pr1 end | _ -> (* cannot occur since we checked that we are in presence of Logic.eq or Jmeq just before *) assert false in - pf_constr_of_global (ConstRef c) + pf_constr_of_global (ConstRef c) else let scheme_name = match dep, lft2rgt, inccl with (* Non dependent case *) @@ -946,12 +946,12 @@ let build_coq_I () = pf_constr_of_global (lib_ref "core.True.I") let rec build_discriminator env sigma true_0 false_0 dirn c = function | [] -> let ind = get_type_of env sigma c in - build_selector env sigma dirn c ind true_0 false_0 + build_selector env sigma dirn c ind true_0 (fst false_0) | ((sp,cnum),argnum)::l -> let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in let newc = mkRel(cnum_nlams-argnum) in let subval = build_discriminator cnum_env sigma true_0 false_0 dirn newc l in - kont sigma subval (false_0,mkProp) + kont sigma subval false_0 (* Note: discrimination could be more clever: if some elimination is not allowed because of a large impredicative constructor in the @@ -983,25 +983,22 @@ let gen_absurdity id = absurd_term=False *) -let ind_scheme_of_eq lbeq = +let ind_scheme_of_eq lbeq to_kind = let (mib,mip) = Global.lookup_inductive (destIndRef lbeq.eq) in - let kind = inductive_sort_family mip in + let from_kind = inductive_sort_family mip in (* use ind rather than case by compatibility *) - let kind = - if kind == InProp then Elimschemes.ind_scheme_kind_from_prop - else Elimschemes.ind_scheme_kind_from_type in + let kind = Elimschemes.nondep_elim_scheme from_kind to_kind in let c, eff = find_scheme kind (destIndRef lbeq.eq) in ConstRef c, eff -let discrimination_pf e (t,t1,t2) discriminator lbeq = +let discrimination_pf e (t,t1,t2) discriminator lbeq to_kind = build_coq_I () >>= fun i -> - build_coq_False () >>= fun absurd_term -> - let eq_elim, eff = ind_scheme_of_eq lbeq in + let eq_elim, eff = ind_scheme_of_eq lbeq to_kind in Proofview.tclEFFECTS eff <*> pf_constr_of_global eq_elim >>= fun eq_elim -> Proofview.tclUNIT - (applist (eq_elim, [t;t1;mkNamedLambda (make_annot e Sorts.Relevant) t discriminator;i;t2]), absurd_term) + (applist (eq_elim, [t;t1;mkNamedLambda (make_annot e Sorts.Relevant) t discriminator;i;t2])) let eq_baseid = Id.of_string "e" @@ -1018,21 +1015,23 @@ let apply_on_clause (f,t) clause = let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = build_coq_True () >>= fun true_0 -> build_coq_False () >>= fun false_0 -> + let false_ty = Retyping.get_type_of env sigma false_0 in + let false_kind = Retyping.get_sort_family_of env sigma false_0 in let e = next_ident_away eq_baseid (vars_of_env env) in let e_env = push_named (Context.Named.Declaration.LocalAssum (make_annot e Sorts.Relevant,t)) env in let discriminator = try Proofview.tclUNIT - (build_discriminator e_env sigma true_0 false_0 dirn (mkVar e) cpath) + (build_discriminator e_env sigma true_0 (false_0,false_ty) dirn (mkVar e) cpath) with UserError _ as ex -> Proofview.tclZERO ex in discriminator >>= fun discriminator -> - discrimination_pf e (t,t1,t2) discriminator lbeq >>= fun (pf, absurd_term) -> - let pf_ty = mkArrow eqn Sorts.Relevant absurd_term in + discrimination_pf e (t,t1,t2) discriminator lbeq false_kind >>= fun pf -> + let pf_ty = mkArrow eqn Sorts.Relevant false_0 in let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in let pf = Clenvtac.clenv_value_cast_meta absurd_clause in - tclTHENS (assert_after Anonymous absurd_term) + tclTHENS (assert_after Anonymous false_0) [onLastHypId gen_absurdity; (Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf)))] let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = |