From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
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) ]) 
 ;;