From a425ea9290454065cf33d33f0ae13a1006fef5fd Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 20 Jul 2009 19:43:42 +0000 Subject: [PATCH] nrewrite now uses the appropriate principle when going from right to left --- .../components/ng_tactics/nTactics.ml | 23 ++++++++++++++++--- 1 file changed, 20 insertions(+), 3 deletions(-) diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 4c5b38369..16602ac9f 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -494,16 +494,33 @@ let elim_tac ~what ~where = exact_tac ("",0,eliminator) status) ]) ;; -let rewrite_tac ~dir ~what:(_,_,what) ~where = +let sort_of_goal_tac sortref = distribute_tac (fun status goal -> + let goalty = get_goalty status goal in + let status,sort = typeof status (ctx_of goalty) goalty in + let status,sort = term_of_cic_term status sort (ctx_of goalty) in + sortref := sort; + status) +;; + +let rewrite_tac ~dir ~what:(_,_,what) ~where status = + let sortref = ref (NCic.Rel 1) in + let status = sort_of_goal_tac sortref status in + let suffix = + match !sortref with + | NCic.Sort NCic.Prop -> "_ind" + | NCic.Sort NCic.Type u -> + "_rect_" ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] !sortref + | _ -> assert false + in let name = - match dir with `LeftToRight -> "eq_elim_r" | `RightToLeft -> "eq_ind" + match dir with `LeftToRight -> "eq_elim_r" | `RightToLeft -> "eq" ^ suffix in block_tac [ select_tac ~where ~job:(`Substexpand 1) true; exact_tac ("",0, Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list Ast.Implicit 5 @ - [what]))] + [what]))] status ;; let intro_tac name = -- 2.39.2