diff options
Diffstat (limited to 'plugins/rtauto')
| -rw-r--r-- | plugins/rtauto/g_rtauto.ml4 | 2 | ||||
| -rw-r--r-- | plugins/rtauto/proof_search.ml | 6 | ||||
| -rw-r--r-- | plugins/rtauto/refl_tauto.ml | 30 | ||||
| -rw-r--r-- | plugins/rtauto/refl_tauto.mli | 6 |
4 files changed, 25 insertions, 19 deletions
diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4 index d27b04834e..7e58ef9a3e 100644 --- a/plugins/rtauto/g_rtauto.ml4 +++ b/plugins/rtauto/g_rtauto.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open Ltac_plugin + DECLARE PLUGIN "rtauto_plugin" TACTIC EXTEND rtauto diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 8b92611136..1ad4d622b2 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -505,12 +505,12 @@ let pp_mapint map = pp_form obj ++ str " => " ++ pp_list (fun (i,f) -> pp_form f) l ++ cut ()) ) map; - str "{ " ++ vb 0 ++ (!pp) ++ str " }" ++ close () + str "{ " ++ hv 0 (!pp ++ str " }") let pp_connect (i,j,f1,f2) = pp_form f1 ++ str " => " ++ pp_form f2 let pp_gl gl= cut () ++ - str "{ " ++ vb 0 ++ + str "{ " ++ hv 0 ( begin match gl.abs with None -> str "" @@ -520,7 +520,7 @@ let pp_gl gl= cut () ++ str "norev =" ++ pp_intmap gl.norev_hyps ++ cut () ++ str "arrows=" ++ pp_mapint gl.right ++ cut () ++ str "cnx =" ++ pp_list pp_connect gl.cnx ++ cut () ++ - str "goal =" ++ pp_form gl.gl ++ str " }" ++ close () + str "goal =" ++ pp_form gl.gl ++ str " }") let pp = function diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 4ed9079517..3655df8951 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -8,6 +8,7 @@ module Search = Explore.Make(Proof_search) +open Ltac_plugin open CErrors open Util open Term @@ -66,19 +67,18 @@ let l_E_Or = lazy (constant "E_Or") let l_D_Or = lazy (constant "D_Or") -let special_whd gl= - let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in - (fun t -> CClosure.whd_val infos (CClosure.inject t)) +let special_whd gl c = + Reductionops.clos_whd_flags CClosure.all (pf_env gl) (Tacmach.project gl) c -let special_nf gl= - let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in - (fun t -> CClosure.norm_val infos (CClosure.inject t)) +let special_nf gl c = + Reductionops.clos_norm_flags CClosure.betaiotazeta (pf_env gl) (Tacmach.project gl) c type atom_env= {mutable next:int; mutable env:(constr*int) list} let make_atom atom_env term= + let term = EConstr.Unsafe.to_constr term in try let (_,i)= List.find (fun (t,_)-> eq_constr term t) atom_env.env @@ -90,13 +90,16 @@ let make_atom atom_env term= Atom i let rec make_form atom_env gls term = + let open EConstr in + let open Vars in let normalize=special_nf gls in let cciterm=special_whd gls term in - match kind_of_term cciterm with + let sigma = Tacmach.project gls in + match EConstr.kind sigma cciterm with Prod(_,a,b) -> - if not (Termops.dependent (mkRel 1) b) && + if noccurn sigma 1 b && Retyping.get_sort_family_of - (pf_env gls) (Tacmach.project gls) a == InProp + (pf_env gls) sigma a == InProp then let fa=make_form atom_env gls a in let fb=make_form atom_env gls b in @@ -113,7 +116,7 @@ let rec make_form atom_env gls term = | App(hd,argv) when Int.equal (Array.length argv) 2 -> begin try - let ind, _ = destInd hd in + let ind, _ = destInd sigma hd in if Names.eq_ind ind (fst (Lazy.force li_and)) then let fa=make_form atom_env gls argv.(0) in let fb=make_form atom_env gls argv.(1) in @@ -134,7 +137,7 @@ let rec make_hyps atom_env gls lenv = function | LocalAssum (id,typ)::rest -> let hrec= make_hyps atom_env gls (typ::lenv) rest in - if List.exists (Termops.dependent (mkVar id)) lenv || + if List.exists (fun c -> Termops.local_occur_var Evd.empty (** FIXME *) id c) lenv || (Retyping.get_sort_family_of (pf_env gls) (Tacmach.project gls) typ != InProp) then @@ -263,7 +266,7 @@ let rtauto_tac gls= let _= if Retyping.get_sort_family_of (pf_env gls) (Tacmach.project gls) gl != InProp - then errorlabstrm "rtauto" (Pp.str "goal should be in Prop") in + then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in let glf=make_form gamma gls gl in let hyps=make_hyps gamma gls [gl] (pf_hyps gls) in let formula= @@ -282,7 +285,7 @@ let rtauto_tac gls= let prf = try project (search_fun (init_state [] formula)) with Not_found -> - errorlabstrm "rtauto" (Pp.str "rtauto couldn't find any proof") in + user_err ~hdr:"rtauto" (Pp.str "rtauto couldn't find any proof") in let search_end_time = System.get_time () in let _ = if !verbose then begin @@ -312,6 +315,7 @@ let rtauto_tac gls= str "Giving proof term to Coq ... ") end in let tac_start_time = System.get_time () in + let term = EConstr.of_constr term in let result= if !check then Proofview.V82.of_tactic (Tactics.exact_check term) gls diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli index 9a14ac6c79..0925523641 100644 --- a/plugins/rtauto/refl_tauto.mli +++ b/plugins/rtauto/refl_tauto.mli @@ -12,13 +12,13 @@ type atom_env= mutable env:(Term.constr*int) list} val make_form : atom_env -> - Proof_type.goal Tacmach.sigma -> Term.types -> Proof_search.form + Proof_type.goal Tacmach.sigma -> EConstr.types -> Proof_search.form val make_hyps : atom_env -> Proof_type.goal Tacmach.sigma -> - Term.types list -> - Context.Named.t -> + EConstr.types list -> + EConstr.named_context -> (Names.Id.t * Proof_search.form) list val rtauto_tac : Proof_type.tactic |