diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/merge.ml | 14 | ||||
| -rw-r--r-- | plugins/omega/coq_omega.ml | 4 | ||||
| -rw-r--r-- | plugins/quote/quote.ml | 71 |
3 files changed, 46 insertions, 43 deletions
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index b2c8489ce..763443717 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -133,20 +133,6 @@ let prNamedRLDecl s lc = prstr "\n"; end -let showind (id:Id.t) = - let cstrid = Constrintern.global_reference id in - let (ind1, u),cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty (EConstr.of_constr cstrid) in - let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) ind1 in - let u = EConstr.Unsafe.to_instance u in - List.iter (fun decl -> - print_string (string_of_name (Context.Rel.Declaration.get_name decl) ^ ":"); - prconstr (RelDecl.get_type decl); print_string "\n") - ib1.mind_arity_ctxt; - Printf.printf "arity :"; prconstr (Inductiveops.type_of_inductive (Global.env ()) (ind1, u)); - Array.iteri - (fun i x -> Printf.printf"type constr %d :" i ; prconstr x) - ib1.mind_user_lc - (** {2 Misc} *) exception Found of int diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index ee748567b..d7408e88e 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -39,10 +39,10 @@ open OmegaSolver let elim_id id = Proofview.Goal.enter { enter = begin fun gl -> - simplest_elim (Tacmach.New.pf_global id gl) + simplest_elim (mkVar id) end } let resolve_id id = Proofview.Goal.enter { enter = begin fun gl -> - apply (Tacmach.New.pf_global id gl) + apply (mkVar id) end } let timing timer_name f arg = f arg diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 7412de1e8..ba8356b52 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -456,39 +456,56 @@ let quote_terms env sigma ivs lc = term. Ring for example needs that, but Ring doesn't use Quote yet. *) +let pf_constrs_of_globals l = + let rec aux l acc = + match l with + [] -> Proofview.tclUNIT (List.rev acc) + | hd :: tl -> + Tacticals.New.pf_constr_of_global hd >>= fun g -> aux tl (g :: acc) + in aux l [] + let quote f lid = - Proofview.Goal.nf_enter { enter = begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let f = Tacmach.New.pf_global f gl in - let cl = List.map (fun id -> EConstr.to_constr sigma (Tacmach.New.pf_global id gl)) lid in - let ivs = compute_ivs f cl gl in - let concl = Proofview.Goal.concl gl in - let quoted_terms = quote_terms env sigma ivs [concl] in - let (p, vm) = match quoted_terms with + Proofview.Goal.enter { enter = begin fun gl -> + let fg = Tacmach.New.pf_global f gl in + let clg = List.map (fun id -> Tacmach.New.pf_global id gl) lid in + Tacticals.New.pf_constr_of_global fg >>= fun f -> + pf_constrs_of_globals clg >>= fun cl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let ivs = compute_ivs f (List.map (EConstr.to_constr sigma) cl) gl in + let concl = Proofview.Goal.concl gl in + let quoted_terms = quote_terms env sigma ivs [concl] in + let (p, vm) = match quoted_terms with | [p], vm -> (p,vm) | _ -> assert false - in - match ivs.variable_lhs with - | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast - | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast + in + match ivs.variable_lhs with + | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast + | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast + end } end } let gen_quote cont c f lid = - Proofview.Goal.nf_enter { enter = begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let f = Tacmach.New.pf_global f gl in - let cl = List.map (fun id -> EConstr.to_constr sigma (Tacmach.New.pf_global id gl)) lid in - let ivs = compute_ivs f cl gl in - let quoted_terms = quote_terms env sigma ivs [c] in - let (p, vm) = match quoted_terms with - | [p], vm -> (p,vm) - | _ -> assert false - in - match ivs.variable_lhs with - | None -> cont (mkApp (f, [| p |])) - | Some _ -> cont (mkApp (f, [| vm; p |])) + Proofview.Goal.enter { enter = begin fun gl -> + let fg = Tacmach.New.pf_global f gl in + let clg = List.map (fun id -> Tacmach.New.pf_global id gl) lid in + Tacticals.New.pf_constr_of_global fg >>= fun f -> + pf_constrs_of_globals clg >>= fun cl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let cl = List.map (EConstr.to_constr sigma) cl in + let ivs = compute_ivs f cl gl in + let quoted_terms = quote_terms env sigma ivs [c] in + let (p, vm) = match quoted_terms with + | [p], vm -> (p,vm) + | _ -> assert false + in + match ivs.variable_lhs with + | None -> cont (mkApp (f, [| p |])) + | Some _ -> cont (mkApp (f, [| vm; p |])) + end } end } (*i |