diff options
Diffstat (limited to 'plugins/rtauto')
| -rw-r--r-- | plugins/rtauto/refl_tauto.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index e66fa10d5b..f1fa694356 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -131,7 +131,7 @@ let rec make_hyps atom_env gls lenv = function | LocalAssum (id,typ)::rest -> let hrec= make_hyps atom_env gls (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 c) lenv || (Retyping.get_sort_family_of (pf_env gls) (Tacmach.project gls) typ != InProp) then |