diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-11 19:52:48 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:28:44 +0100 |
| commit | cbea91d815f134d63d02d8fb1bd78ed97db28cd1 (patch) | |
| tree | adeb71808e2f4d6be1686071e79e96cf6761f3c0 /toplevel | |
| parent | 53fe23265daafd47e759e73e8f97361c7fdd331b (diff) | |
Tacmach API using EConstr.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 4 | ||||
| -rw-r--r-- | toplevel/command.ml | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 02c43aec5..6561627f6 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -363,7 +363,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = ) in Proofview.Goal.nf_enter { enter = begin fun gl -> - let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl p) gl in + let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl (EConstr.of_constr p)) gl in let u,v = destruct_ind type_of_pq in let lb_type_of_p = try @@ -425,7 +425,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = match (l1,l2) with | (t1::q1,t2::q2) -> Proofview.Goal.enter { enter = begin fun gl -> - let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in + let tt1 = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr t1) in if eq_constr t1 t2 then aux q1 q2 else ( let u,v = try destruct_ind tt1 diff --git a/toplevel/command.ml b/toplevel/command.ml index dbf256ba8..80f3b26e4 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1164,7 +1164,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps)))) fixnames fixtypes fiximps in let init_tac = - Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC) + Some (List.map (Option.cata (EConstr.of_constr %> Tacmach.refine_no_check) Tacticals.tclIDTAC) fixdefs) in let init_tac = Option.map (List.map Proofview.V82.tactic) init_tac @@ -1201,7 +1201,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps)))) fixnames fixtypes fiximps in let init_tac = - Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC) + Some (List.map (Option.cata (EConstr.of_constr %> Tacmach.refine_no_check) Tacticals.tclIDTAC) fixdefs) in let init_tac = Option.map (List.map Proofview.V82.tactic) init_tac |