Use of standard OCaml syntax

[helm.git] / matita / components / ng_tactics / nDestructTac.ml

diff --git a/matita/components/ng_tactics/nDestructTac.ml b/matita/components/ng_tactics/nDestructTac.ml
index f03baa65645b5bf1e9ee33414fc0b47f89040319..ab62618642f23b60b875a8c71538cdfa3a84e647 100644 (file)
--- a/matita/components/ng_tactics/nDestructTac.ml
+++ b/matita/components/ng_tactics/nDestructTac.ml
@@ -130,29 +130,29 @@ let arg_list nleft t =
 
 let nargs it nleft consno =
   pp (lazy (Printf.sprintf "nargs %d %d" nleft consno));
-  let _,indname,_,cl = it in
+  let _,_indname,_,cl = it in
   let _,_,t_k = List.nth cl consno in
   List.length (arg_list nleft t_k) ;;
 
 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
@@ -327,14 +327,14 @@ let mk_discriminator ~use_jmeq ?(force=false) name it leftno status baseuri =
       NotationPt.Theorem
        (name, principle, Some (NotationPt.Implicit (`Tagged "inv")), attrs))
   in 
-  let uri,height,nmenv,nsubst,nobj = theorem in
+  let _uri,_height,nmenv,_nsubst,_nobj = theorem in
   let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
   let status = status#set_obj theorem in
   let status = status#set_stack ninitial_stack in
   let status = subst_metasenv_and_fix_names status in
 
   (* PHASE 3: we finally prove the discrimination principle *)
-  let dbranch it ~use_jmeq leftno consno =
+  let dbranch it ~use_jmeq:__ leftno consno =
     let refl_id = mk_sym "refl" in
     pp (lazy (Printf.sprintf "dbranch %d %d" leftno consno));
     let nlist = HExtlib.list_seq 0 (nargs it leftno consno) in
@@ -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
@@ -482,7 +482,7 @@ let subst_tac ~context ~dir skip cur_eq =
     else 
     let gen_tac x =
       (fun s -> 
-      let x' = String.concat " " x in
+      (*let x' = String.concat " " x in*)
       let x = List.map mk_id x in
       (* let s = NTactics.print_tac false ("@generalize " ^ x') s in *)
       generalize0_tac x s) in
@@ -619,7 +619,7 @@ let select_eq ctx acc domain status goal =
            | _ -> status, `NonEq 
            in match kind with
               | `Identity ->
-                  let status, goalty = term_of_cic_term status (get_goalty status goal) ctx in
+                  let status, _goalty = term_of_cic_term status (get_goalty status goal) ctx in
                      status, Some (List.length ctx - i), kind
               | `Cycle | `Blob | `NonEq -> aux (i+1) (* XXX: skip cyclic/blob equations for now *)
               | _ ->