diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/firstorder/sequent.ml | 8 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 12 |
2 files changed, 12 insertions, 8 deletions
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 3dd5059e5d..db3631daa4 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -205,10 +205,10 @@ open Hints let extend_with_auto_hints env sigma l seq = let f (seq,sigma) p_a_t = - match repr_hint p_a_t.code with - | Res_pf (c,_) | Give_exact (c,_) - | Res_pf_THEN_trivial_fail (c,_) -> - let (c, _, _) = c in + match FullHint.repr p_a_t with + | Res_pf c | Give_exact c + | Res_pf_THEN_trivial_fail c -> + let c = c.hint_term in (match EConstr.destRef sigma c with | exception Constr.DestKO -> seq, sigma | gr, _ -> diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 29a9c65561..da623703a2 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -389,17 +389,21 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_ ppdebug(lazy Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty)); try Proofview.V82.of_tactic (refine_with ~first_goes_last:(not !ssroldreworder || under) ~with_evars:under (sigma, proof)) gl - with _ -> + with e when CErrors.noncritical e -> (* we generate a msg like: "Unable to find an instance for the variable" *) let hd_ty, miss = match EConstr.kind sigma c with | App (hd, args) -> let hd_ty = Retyping.get_type_of env sigma hd in - let names = let rec aux t = function 0 -> [] | n -> + let names = let rec aux env t = function 0 -> [] | n -> let t = Reductionops.whd_all env sigma t in let open EConstr in match kind_of_type sigma t with - | ProdType (name, _, t) -> name.binder_name :: aux t (n-1) - | _ -> assert false in aux hd_ty (Array.length args) in + | ProdType (name, ty, t) -> + name.binder_name :: + aux (EConstr.push_rel (Context.Rel.Declaration.LocalAssum (name,ty)) env) t (n-1) + | _ -> + (* In the case the head is an HO constant it may accept more arguments *) + CList.init n (fun _ -> Names.Name.Anonymous) in aux env hd_ty (Array.length args) in hd_ty, Util.List.map_filter (fun (t, name) -> let evs = Evar.Set.elements (Evarutil.undefined_evars_of_term sigma t) in let open_evs = List.filter (fun k -> |