From: Claudio Sacerdoti Coen Date: Mon, 29 Nov 2010 12:49:26 +0000 (+0000) Subject: Back-porting from new Matita: X-Git-Tag: make_still_working~2681 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=186638106f23401e88e512a4a6dfd07d73d8be04;p=helm.git 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. --- 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) ]) ;;