tab -> spaces

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 1b5f407bc31c2cdfddd5814c7346dc5c64b5a6b0..b185d693cf14f02e086e89e07f19d7ca0642a0c3 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -234,11 +234,11 @@ let
          [],[] -> []
        | uri::tl,[] ->
           let ty =
-           let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+            let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
               match o with
-                 C.Variable (_,_,ty,_,_) ->
-                   CicSubstitution.subst_vars !exp_named_subst_diff ty
-               | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
+                  C.Variable (_,_,ty,_,_) ->
+                    CicSubstitution.subst_vars !exp_named_subst_diff ty
+                | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
           in
 (* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type to simulate ?1 :< Type
            (match ty with
@@ -249,7 +249,7 @@ let
                   let subst_item = uri,C.Meta (fresh_meta',[]) in
                    newmetasenvfragment :=
                     (fresh_meta,[],C.Sort (C.Type (CicUniv.fresh()))) ::
-                    (* TASSI: ?? *)
+                     (* TASSI: ?? *)
                      (fresh_meta',[],C.Meta (fresh_meta,[])) :: !newmetasenvfragment ;
                    exp_named_subst_diff := !exp_named_subst_diff @ [subst_item] ;
                    subst_item::(aux (tl,[]))
@@ -355,7 +355,7 @@ let apply_tac_verbose ~term (proof, goal) =
 (*    prerr_endline ("me: " ^ CicMetaSubst.ppmetasenv newmetasenv'' subst); *)
    let subst_in =
      (* if we just apply the subtitution, the type is irrelevant:
-             we may use Implicit, since it will be dropped *)
+              we may use Implicit, since it will be dropped *)
      CicMetaSubst.apply_subst ((metano,(context,bo',Cic.Implicit None))::subst)
    in
    let (newproof, newmetasenv''') = 
@@ -501,7 +501,6 @@ let elim_tac ~term =
    let (curi,metasenv,proofbo,proofty) = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
     let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
-      (* TASSI: FIXME *)
     let uri,exp_named_subst,typeno,args =
      match termty with
         C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
@@ -512,7 +511,7 @@ let elim_tac ~term =
      let eliminator_uri =
       let buri = U.buri_of_uri uri in
       let name = 
-       let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+        let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
        match o with
           C.InductiveDefinition (tys,_,_,_) ->
            let (name,_,_,_) = List.nth tys typeno in
@@ -520,7 +519,6 @@ let elim_tac ~term =
         | _ -> assert false
       in
       let ty_ty,_ = T.type_of_aux' metasenv context ty CicUniv.empty_ugraph in
-       (* TASSI: FIXME *)
       let ext =
        match ty_ty with
           C.Sort C.Prop -> "_ind"
@@ -534,7 +532,7 @@ let elim_tac ~term =
      in
       let eliminator_ref = C.Const (eliminator_uri,exp_named_subst) in
        let ety,_ = 
-        T.type_of_aux' metasenv context eliminator_ref CicUniv.empty_ugraph in
+         T.type_of_aux' metasenv context eliminator_ref CicUniv.empty_ugraph in
         let rec find_args_no =
          function
             C.Prod (_,_,t) -> 1 + find_args_no t
@@ -553,9 +551,9 @@ let elim_tac ~term =
          in
           let metasenv', term_to_refine' =
            CicMkImplicit.expand_implicits metasenv [] context term_to_refine in
-          let refined_term,_,metasenv'',_ = (* TASSI: FIXME *)
+          let refined_term,_,metasenv'',_ = 
            CicRefine.type_of_aux' metasenv' context term_to_refine' 
-            CicUniv.empty_ugraph
+             CicUniv.empty_ugraph
           in
            let new_goals =
             ProofEngineHelpers.compare_metasenvs