diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-06 19:05:19 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-06 19:14:33 +0100 |
| commit | 8972a5ed75b7778ad992ef018b163c6ac6e27297 (patch) | |
| tree | 6fe6ca6b9ad22b4927dd711ea7a60e33cfd33b75 /plugins/funind | |
| parent | 2c5e81e3bc6ec17d253aeedd1b2bf4ccd3b81933 (diff) | |
Getting rid of pf_is_matching in Funind.
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/recdef.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index b0a76137b..766adfc63 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -141,7 +141,7 @@ let def_id = Id.of_string "def" let p_id = Id.of_string "p" let rec_res_id = Id.of_string "rec_res";; let lt = function () -> (coq_init_constant "lt") -let le = function () -> (coq_init_constant "le") +let le = function () -> (Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules "le") let ex = function () -> (coq_init_constant "ex") let nat = function () -> (coq_init_constant "nat") let iter_ref () = @@ -857,9 +857,13 @@ let rec prove_le g = Proofview.V82.of_tactic (apply (delayed_force le_n)); begin try - let matching_fun = - pf_is_matching g - (Pattern.PApp(Pattern.PRef (Globnames.global_of_constr (EConstr.Unsafe.to_constr (le ()))),[|Pattern.PVar (destVar sigma x);Pattern.PMeta None|])) in + let matching_fun c = match EConstr.kind sigma c with + | App (c, [| x0 ; _ |]) -> + EConstr.isVar sigma x0 && + Id.equal (destVar sigma x0) (destVar sigma x) && + is_global sigma (le ()) c + | _ -> false + in let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) in let y = |