diff options
Diffstat (limited to 'plugins/rtauto')
| -rw-r--r-- | plugins/rtauto/refl_tauto.ml | 5 | ||||
| -rw-r--r-- | plugins/rtauto/refl_tauto.mli | 2 |
2 files changed, 4 insertions, 3 deletions
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index a6b6c57ff9..89528fe357 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -16,6 +16,7 @@ open CErrors open Util open Term open Constr +open Context open Proof_search open Context.Named.Declaration @@ -127,7 +128,7 @@ let rec make_hyps env sigma atom_env lenv = function | LocalAssum (id,typ)::rest -> let hrec= make_hyps env sigma atom_env (typ::lenv) rest in - if List.exists (fun c -> Termops.local_occur_var Evd.empty (* FIXME *) id c) lenv || + if List.exists (fun c -> Termops.local_occur_var Evd.empty (* FIXME *) id.binder_name c) lenv || (Retyping.get_sort_family_of env sigma typ != InProp) then hrec @@ -291,7 +292,7 @@ let rtauto_tac = build_form formula; build_proof [] 0 prf|]) in let term= - applistc main (List.rev_map (fun (id,_) -> mkVar id) hyps) in + applistc main (List.rev_map (fun (id,_) -> mkVar id.binder_name) hyps) in let build_end_time=System.get_time () in let () = if !verbose then begin diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli index 49b5ee5ac7..3de0ba44df 100644 --- a/plugins/rtauto/refl_tauto.mli +++ b/plugins/rtauto/refl_tauto.mli @@ -23,6 +23,6 @@ val make_hyps -> atom_env -> EConstr.types list -> EConstr.named_context - -> (Names.Id.t * Proof_search.form) list + -> (Names.Id.t Context.binder_annot * Proof_search.form) list val rtauto_tac : unit Proofview.tactic |