From dbe5d5ee749b3d5d36c91f96b73d7554967fc8cd Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 25 Oct 2005 15:48:18 +0000 Subject: [PATCH] fixed lapply on new tinycals semantic removed expand_implicits from elim --- helm/ocaml/tactics/fwdSimplTactic.ml | 6 +++--- helm/ocaml/tactics/primitiveTactics.ml | 4 +--- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml index 16510a7cd..a5c7878c7 100644 --- a/helm/ocaml/tactics/fwdSimplTactic.ml +++ b/helm/ocaml/tactics/fwdSimplTactic.ml @@ -107,8 +107,8 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub let conclusion = match metas with [] -> what | _ -> Cic.Appl (what :: List.rev metas) in - let tac = T.thens ~start:(letin_tac conclusion) - ~continuations:[clearbody ~index:1] + let tac = T.then_ ~start:(letin_tac conclusion) + ~continuation:(clearbody ~index:1) in let proof = (xuri, metasenv, u, t) in let aux (proof, goals) (tac, goal) = @@ -137,7 +137,7 @@ let fwd_simpl_tac | uri :: _ -> Printf.eprintf "fwd: %s\n" (UriManager.string_of_uri uri); flush stderr; let start = lapply_tac (Cic.Rel index) (Cic.Const (uri, [])) in - let tac = T.thens ~start ~continuations:[PESR.clear hyp] in + let tac = T.then_ ~start ~continuation:(PESR.clear hyp) in PET.apply_tactic tac status in PET.mk_tactic fwd_simpl_tac diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index d26221d39..96ff130c5 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -517,10 +517,8 @@ let elim_tac ~term = in C.Appl (eliminator_ref :: make_tl term (args_no - 1)) in - let metasenv', term_to_refine' = - CicMkImplicit.expand_implicits metasenv' [] context term_to_refine in let refined_term,_,metasenv'',_ = - CicRefine.type_of_aux' metasenv' context term_to_refine' + CicRefine.type_of_aux' metasenv' context term_to_refine CicUniv.empty_ugraph in let new_goals = -- 2.39.2