-let setoid_reflexivity (*COQgl*) =
- try
- let relation_class =
- relation_class_that_matches_a_constr "Setoid_reflexivity"
- [] ((*COQ pf_concl gl*) assert false) in
- match relation_class with
- Leibniz _ -> assert false (* since [] is empty *)
- | Relation rel ->
- match rel.rel_refl with
- None ->
- raise (ProofEngineTypes.Fail (lazy
- ("The relation " ^ prrelation rel ^ " is not reflexive.")))
- | Some refl -> (*COQ apply refl gl*) assert false
- with
- Optimize -> (*COQ reflexivity gl*) assert false
+let setoid_reflexivity_tac =
+ let tac ((proof,goal) as status) =
+ let (_,metasenv,_subst,_,_, _) = proof in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+ try
+ let relation_class =
+ relation_class_that_matches_a_constr "Setoid_reflexivity" [] ty in
+ match relation_class with
+ Leibniz _ -> assert false (* since [] is empty *)
+ | Relation rel ->
+ match rel.rel_refl with
+ None ->
+ raise (ProofEngineTypes.Fail (lazy
+ ("The relation " ^ prrelation rel ^ " is not reflexive.")))
+ | Some refl ->
+ ProofEngineTypes.apply_tactic (PrimitiveTactics.apply_tac refl)
+ status
+ with
+ Optimize ->
+ ProofEngineTypes.apply_tactic EqualityTactics.reflexivity_tac status
+ in
+ ProofEngineTypes.mk_tactic tac