diff options
Diffstat (limited to 'plugins/firstorder/sequent.ml')
| -rw-r--r-- | plugins/firstorder/sequent.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 72bde18f4..c0e5c7e58 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -199,7 +199,7 @@ let expand_constructor_hints = let extend_with_ref_list l seq gl= let l = expand_constructor_hints l in let f gr seq= - let c=constr_of_global gr in + let c=Universes.constr_of_global gr in let typ=(pf_type_of gl c) in add_formula Hyp gr typ seq gl in List.fold_right f l seq @@ -210,10 +210,10 @@ let extend_with_auto_hints l seq gl= let seqref=ref seq in let f p_a_t = match p_a_t.code with - Res_pf (c,_) | Give_exact c + Res_pf (c,_) | Give_exact (c,_) | Res_pf_THEN_trivial_fail (c,_) -> (try - let gr=global_of_constr c in + let gr = global_of_constr c in let typ=(pf_type_of gl c) in seqref:=add_formula Hint gr typ !seqref gl with Not_found->()) |