X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnDestructTac.ml;h=ab62618642f23b60b875a8c71538cdfa3a84e647;hb=8a5c30a914d7ff665218b31853c6fb4bcf58aa08;hp=f25114817de9256f58ed85eb66167a38f30b3daa;hpb=d7aca3eacb4bd8dc56223098f92e5370c82f92ff;p=helm.git

diff --git a/matita/components/ng_tactics/nDestructTac.ml b/matita/components/ng_tactics/nDestructTac.ml
index f25114817..ab6261864 100644
--- a/matita/components/ng_tactics/nDestructTac.ml
+++ b/matita/components/ng_tactics/nDestructTac.ml
@@ -136,23 +136,23 @@ let nargs it nleft consno =
 
 let default_pattern = "",0,(None,[],Some NotationPt.UserInput);; 
 let prod_pattern = 
-  "",0,(None,[],Some NotationPt.Binder 
+  "",0,(None,[],Some (NotationPt.Binder 
     (`Pi, (mk_id "_",Some (NotationPt.Appl
       [ NotationPt.Implicit `JustOne
       ; NotationPt.Implicit `JustOne
       ; NotationPt.UserInput
       ; NotationPt.Implicit `JustOne ])), 
-  NotationPt.Implicit `JustOne));;
+  NotationPt.Implicit `JustOne)));;
 
 let prod_pattern_jm = 
-  "",0,(None,[],Some NotationPt.Binder 
+  "",0,(None,[],Some (NotationPt.Binder 
     (`Pi, (mk_id "_",Some (NotationPt.Appl
       [ NotationPt.Implicit `JustOne
       ; NotationPt.Implicit `JustOne
       ; NotationPt.UserInput
       ; NotationPt.Implicit `JustOne
       ; NotationPt.Implicit `JustOne ])),
-  NotationPt.Implicit `JustOne));;
+  NotationPt.Implicit `JustOne)));;
 
 let hp_pattern n = 
   "",0,(None,[n, NotationPt.Appl
@@ -448,7 +448,7 @@ let saturate_skip status context skip =
 ;;
       
 let subst_tac ~context ~dir skip cur_eq =
-  fun status as oldstatus ->
+  fun (status as oldstatus) ->
   let eq_name,(NCic.Decl s | NCic.Def (s,_)) = List.nth context (cur_eq-1) in
   let _,ctx' = HExtlib.split_nth cur_eq context in
   let status, s = NTacStatus.whd status ctx' (mk_cic_term ctx' s) in