From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 7 Jul 2005 11:02:10 +0000 (+0000)
Subject: tab -> spaces
X-Git-Tag: V_0_7_1~26
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b62ce94a7d85811d7e843009daf2a52b31993ea7;p=helm.git

tab -> spaces
---

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 1b5f407bc..b185d693c 100644
--- 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