freescale porting

[helm.git] / helm / software / components / ng_tactics / nTactics.ml

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 9834cce8a943e1377ecd0b6728e5dca46506847c..10fa168d492517123eff7b4b18861cb9827cfa47 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -52,7 +52,7 @@ let branch_tac status =
     | [] -> assert false
     | (g, t, k, tag) :: s ->
           match init_pos g with (* TODO *)
-          | [] | [ _ ] -> fail (lazy "too few goals to branch");
+          | [] | [ _ ] -> fail (lazy "too few goals to branch")
           | loc :: loc_tl ->
                ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
   in
@@ -314,7 +314,7 @@ let clear_tac names =
      names
    in
    let n,h,metasenv,subst,o = status#obj in
-   let metasenv,subst,_ = NCicMetaSubst.restrict metasenv subst goal js in
+   let metasenv,subst,_,_ = NCicMetaSubst.restrict metasenv subst goal js in
     status#set_obj (n,h,metasenv,subst,o))
 ;;
 
@@ -368,7 +368,7 @@ let select0_tac ~where:(wanted,hyps,where) ~job  =
    let newgoalty = mk_cic_term newgoalctx newgoalty in
 
    let status, instance = 
-     mk_meta status newgoalctx (`Decl newgoalty) 
+     mk_meta status newgoalctx (`Decl newgoalty) `IsTerm
    in
    instantiate status goal instance)
 ;;
@@ -395,7 +395,6 @@ let generalize_tac ~where =
  let l = ref [] in
  block_tac [ 
    select_tac ~where ~job:(`Collect l) true; 
-   print_tac true "ha selezionato?";
    (fun s -> distribute_tac (fun status goal ->
       let goalty = get_goalty status goal in
       let status,canon,rest =
@@ -423,8 +422,8 @@ let cut_tac t =
  block_tac [ 
   exact_tac ("",0, Ast.Appl [Ast.Implicit `JustOne; Ast.Implicit `JustOne]);
   branch_tac;
-   pos_tac [2]; exact_tac t;
-   shift_tac; pos_tac [1]; skip_tac;
+   pos_tac [3]; exact_tac t;
+   shift_tac; pos_tac [2]; skip_tac;
   merge_tac ]
 ;;
 
@@ -479,6 +478,8 @@ type indtyinfo = {
  }
 ;;
 
+let ref_of_indtyinfo iti = iti.reference;;
+
 let analyze_indty_tac ~what indtyref =
  distribute_tac (fun status goal ->
   let goalty = get_goalty status goal in
@@ -497,7 +498,7 @@ let analyze_indty_tac ~what indtyref =
 let sort_of_goal_tac sortref = distribute_tac (fun status goal ->
   let goalty = get_goalty status goal in
   let status,sort = typeof status (ctx_of goalty) goalty in
-  let sort = fix_sorts sort in
+  let status, sort = fix_sorts status sort in
   let status, sort = term_of_cic_term status sort (ctx_of goalty) in
    sortref := sort;
    status)
@@ -587,7 +588,7 @@ let case1_tac name =
              if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
 ;;
 
-let constructor ?(num=1) ~args status goal = 
+let constructor_tac ?(num=1) ~args = distribute_tac (fun status goal ->
   if num < 1 then fail (lazy "constructor numbers begin with 1");
   let gty = get_goalty status goal in
   let status, (r,_,_,_) = analyse_indty status gty in
@@ -597,11 +598,9 @@ let constructor ?(num=1) ~args status goal =
     Ast.Appl (HExtlib.list_concat ~sep:[Ast.Implicit `Vector]
       ([Ast.NRef ref] :: List.map (fun _,_,x -> [x]) args))
   in
-  exec (apply_tac ("",0,t)) status goal
+  exec (apply_tac ("",0,t)) status goal)
 ;;
 
-let constructor_tac ?num ~args = distribute_tac (constructor ?num ~args);;
-
 let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->
  let gty = get_goalty status goal in
  let eq status ctx t1 t2 =