From 186638106f23401e88e512a4a6dfd07d73d8be04 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 29 Nov 2010 12:49:26 +0000 Subject: [PATCH] Back-porting from new Matita: Bug fixed: analysing inductive type that contains implicit used to duplicate the metas in the metasenv since the term was disambiguated twice, in the analyze and in the tactic that uses the analyze. --- .../components/ng_tactics/nTactics.ml | 22 ++++++++++++------- 1 file changed, 14 insertions(+), 8 deletions(-) diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index c45e825a4..895eec2d2 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -476,6 +476,7 @@ type indtyinfo = { lefts: NCic.term list; rights: NCic.term list; reference: NReference.reference; + term: NCic.term } ;; @@ -489,9 +490,10 @@ let analyze_indty_tac ~what indtyref = let status, (r,consno,lefts,rights) = analyse_indty status ty_what in let leftno = List.length lefts in let rightno = List.length rights in + let status,what = term_of_cic_term status what (ctx_of goalty) in indtyref := Some { rightno = rightno; leftno = leftno; consno = consno; - lefts = lefts; rights = rights; reference = r; + lefts = lefts; rights = rights; reference = r; term = what }; exec id_tac status goal) ;; @@ -523,8 +525,8 @@ let elim_tac ~what:(txt,len,what) ~where = (match !sort with NCic.Sort x -> x | _ -> assert false)) in let eliminator = - let _,_,w = what in - Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ] + let what = (HExtlib.unopt !indtyinfo).term in + Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; Ast.NCic what ] in exact_tac ("",0,eliminator) status) ]) ;; @@ -594,9 +596,13 @@ let cases_tac ~what:(txt,len,what) ~where = atomic_tac (block_tac [ analyze_indty_tac ~what indtyinfo; - (fun s -> select_tac - ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1))true s); - distribute_tac (cases ~what) ]) + (fun s -> + select_tac + ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1))true + s); + (fun s -> + distribute_tac + (cases ~what:("",0,Ast.NCic (HExtlib.unopt !indtyinfo).term)) s); ]) ;; let case1_tac name = @@ -689,8 +695,8 @@ let inversion_tac ~what:(txt,len,what) ~where = (match !sort with NCic.Sort x -> x | _ -> assert false)) in let eliminator = - let _,_,w = what in - Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ] + let what = (HExtlib.unopt !indtyinfo).term in + Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; Ast.NCic what ] in exact_tac ("",0,eliminator) status) ]) ;; -- 2.39.2