[coq] Untabify the whole ML codebase.

We also remove trailing whitespace.

Script used:

```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```

3 files changed, 501 insertions, 501 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 6f8fe8959c..500f464ea7 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -56,7 +56,7 @@ module ST=struct
   module IntPairTable = Hashtbl.Make(IntPair)
 
   type t = {toterm: int IntPairTable.t;
-	    tosign: (int * int) IntTable.t}
+            tosign: (int * int) IntTable.t}
 
   let empty () =
     {toterm=IntPairTable.create init_size;
@@ -64,19 +64,19 @@ module ST=struct
 
   let enter t sign st=
     if IntPairTable.mem st.toterm sign then
-	anomaly ~label:"enter" (Pp.str "signature already entered.")
+        anomaly ~label:"enter" (Pp.str "signature already entered.")
     else
-	IntPairTable.replace st.toterm sign t;
-	IntTable.replace st.tosign t sign
+        IntPairTable.replace st.toterm sign t;
+        IntTable.replace st.tosign t sign
 
   let query sign st=IntPairTable.find st.toterm sign
 
   let delete st t=
     try let sign=IntTable.find st.tosign t in
-	IntPairTable.remove st.toterm sign;
-	IntTable.remove st.tosign t
+        IntPairTable.remove st.toterm sign;
+        IntTable.remove st.tosign t
     with
-	Not_found -> ()
+        Not_found -> ()
 
   let delete_set st s = Int.Set.iter (delete st) s
 
@@ -199,7 +199,7 @@ type quant_eq =
     qe_rhs: ccpattern;
     qe_rhs_valid:patt_kind
   }
-    
+
 let swap eq : equality =
   let swap_rule=match eq.rule with
       Congruence -> Congruence
@@ -234,21 +234,21 @@ type node =
 
 module Constrhash = Hashtbl.Make
   (struct type t = constr
-	  let equal = eq_constr_nounivs
-	  let hash = Constr.hash
+          let equal = eq_constr_nounivs
+          let hash = Constr.hash
    end)
 module Typehash = Constrhash
 
 module Termhash = Hashtbl.Make
   (struct type t = term
-	  let equal = term_equal
-	  let hash = hash_term
+          let equal = term_equal
+          let hash = hash_term
    end)
 
 module Identhash = Hashtbl.Make
   (struct type t = Id.t
-	  let equal = Id.equal
-	  let hash = Id.hash
+          let equal = Id.equal
+          let hash = Id.hash
    end)
 
 type forest=
@@ -293,7 +293,7 @@ let empty_forest() =
     axioms=Constrhash.create init_size;
     syms=Termhash.create init_size
   }
-    
+
 let empty depth gls:state =
   {
     uf= empty_forest ();
@@ -311,7 +311,7 @@ let empty depth gls:state =
     env=pf_env gls;
     sigma=project gls
   }
-    
+
 let forest state = state.uf
 
 let compress_path uf i j = uf.map.(j).cpath<-i
@@ -332,11 +332,11 @@ let get_constructors uf i= uf.map.(i).constructors
 
 let rec find_oldest_pac uf i pac=
   try PacMap.find pac (get_constructors uf i) with
-    Not_found -> 
-      match uf.map.(i).clas with 
-	Eqto (j,_) -> find_oldest_pac uf j pac
+    Not_found ->
+      match uf.map.(i).clas with
+        Eqto (j,_) -> find_oldest_pac uf j pac
       | Rep _ -> raise Not_found
-     
+
 
 let get_constructor_info uf i=
   match uf.map.(i).term with
@@ -397,11 +397,11 @@ let next uf=
     if Int.equal nsize uf.max_size then
       let newmax=uf.max_size * 3 / 2 + 1 in
       let newmap=Array.make newmax dummy_node in
-	begin
-	  uf.max_size<-newmax;
-	  Array.blit uf.map 0 newmap 0 size;
-	  uf.map<-newmap
-	end
+        begin
+          uf.max_size<-newmax;
+          Array.blit uf.map 0 newmap 0 size;
+          uf.map<-newmap
+        end
     else ();
     uf.size<-nsize;
     size
@@ -440,14 +440,14 @@ let rec canonize_name sigma c =
   let func c = canonize_name sigma (EConstr.of_constr c) in
     match Constr.kind c with
       | Const (kn,u) ->
-	  let canon_const = Constant.make1 (Constant.canonical kn) in 
-	    (mkConstU (canon_const,u))
+          let canon_const = Constant.make1 (Constant.canonical kn) in
+            (mkConstU (canon_const,u))
       | Ind ((kn,i),u) ->
-	  let canon_mind = MutInd.make1 (MutInd.canonical kn) in
-	    (mkIndU ((canon_mind,i),u))
+          let canon_mind = MutInd.make1 (MutInd.canonical kn) in
+            (mkIndU ((canon_mind,i),u))
       | Construct (((kn,i),j),u) ->
-	  let canon_mind = MutInd.make1 (MutInd.canonical kn) in
-	    mkConstructU (((canon_mind,i),j),u)
+          let canon_mind = MutInd.make1 (MutInd.canonical kn) in
+            mkConstructU (((canon_mind,i),j),u)
       | Prod (na,t,ct) ->
           mkProd (na,func t, func ct)
       | Lambda (na,t,ct) ->
@@ -457,9 +457,9 @@ let rec canonize_name sigma c =
       | App (ct,l) ->
           mkApp (func ct,Array.Smart.map func l)
       | Proj(p,c) ->
-	let p' = Projection.map (fun kn ->
+        let p' = Projection.map (fun kn ->
           MutInd.make1 (MutInd.canonical kn)) p in
-	  (mkProj (p', func c))
+          (mkProj (p', func c))
       | _ -> c
 
 (* rebuild a term from a pattern and a substitution *)
@@ -477,8 +477,8 @@ let rec inst_pattern subst = function
       subst.(pred i)
   | PApp (t, args) ->
       List.fold_right
-	(fun spat f -> Appli (f,inst_pattern subst spat))
-	   args t
+        (fun spat f -> Appli (f,inst_pattern subst spat))
+           args t
 
 let pr_idx_term env sigma uf i = str "[" ++ int i ++ str ":=" ++
   Printer.pr_econstr_env env sigma (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]"
@@ -489,62 +489,62 @@ let pr_term env sigma t = str "[" ++
 let rec add_term state t=
   let uf=state.uf in
     try Termhash.find uf.syms t with
-	Not_found ->
-	  let b=next uf in
+        Not_found ->
+          let b=next uf in
           let trm = constr_of_term t in
           let typ = Typing.unsafe_type_of state.env state.sigma (EConstr.of_constr trm) in
           let typ = canonize_name state.sigma typ in
-	  let new_node=
-	    match t with
-		Symb _ | Product (_,_) ->
-		  let paf =
-		    {fsym=b;
-		     fnargs=0} in
-		    Queue.add (b,Fmark paf) state.marks;
-		    {clas= Rep (new_representative typ);
-		     cpath= -1;
-		     constructors=PacMap.empty;
-		     vertex= Leaf;
-		     term= t}
-	      | Eps id ->
-		  {clas= Rep (new_representative typ);
-		   cpath= -1;
-		   constructors=PacMap.empty;
-		   vertex= Leaf;
-		   term= t}
-	      | Appli (t1,t2) ->
-		  let i1=add_term state t1 and i2=add_term state t2 in
-		    add_lfather uf (find uf i1) b;
-		    add_rfather uf (find uf i2) b;
-		    state.terms<-Int.Set.add b state.terms;
-		    {clas= Rep (new_representative typ);
-		     cpath= -1;
-		     constructors=PacMap.empty;
-		     vertex= Node(i1,i2);
-		     term= t}
-	      | Constructor cinfo ->
-		  let paf =
-		    {fsym=b;
-		     fnargs=0} in
-		    Queue.add (b,Fmark paf) state.marks;
-		  let pac =
-		    {cnode= b;
-		     arity= cinfo.ci_arity;
-		     args=[]} in
-		    Queue.add (b,Cmark pac) state.marks;
-		    {clas=Rep (new_representative typ);
-		     cpath= -1;
-		     constructors=PacMap.empty;
-		     vertex=Leaf;
-		     term=t}
-	  in
-	    uf.map.(b)<-new_node;
-	    Termhash.add uf.syms t b;
-	    Typehash.replace state.by_type typ
-	      (Int.Set.add b
-		 (try Typehash.find state.by_type typ with
-		      Not_found -> Int.Set.empty));
-	    b
+          let new_node=
+            match t with
+                Symb _ | Product (_,_) ->
+                  let paf =
+                    {fsym=b;
+                     fnargs=0} in
+                    Queue.add (b,Fmark paf) state.marks;
+                    {clas= Rep (new_representative typ);
+                     cpath= -1;
+                     constructors=PacMap.empty;
+                     vertex= Leaf;
+                     term= t}
+              | Eps id ->
+                  {clas= Rep (new_representative typ);
+                   cpath= -1;
+                   constructors=PacMap.empty;
+                   vertex= Leaf;
+                   term= t}
+              | Appli (t1,t2) ->
+                  let i1=add_term state t1 and i2=add_term state t2 in
+                    add_lfather uf (find uf i1) b;
+                    add_rfather uf (find uf i2) b;
+                    state.terms<-Int.Set.add b state.terms;
+                    {clas= Rep (new_representative typ);
+                     cpath= -1;
+                     constructors=PacMap.empty;
+                     vertex= Node(i1,i2);
+                     term= t}
+              | Constructor cinfo ->
+                  let paf =
+                    {fsym=b;
+                     fnargs=0} in
+                    Queue.add (b,Fmark paf) state.marks;
+                  let pac =
+                    {cnode= b;
+                     arity= cinfo.ci_arity;
+                     args=[]} in
+                    Queue.add (b,Cmark pac) state.marks;
+                    {clas=Rep (new_representative typ);
+                     cpath= -1;
+                     constructors=PacMap.empty;
+                     vertex=Leaf;
+                     term=t}
+          in
+            uf.map.(b)<-new_node;
+            Termhash.add uf.syms t b;
+            Typehash.replace state.by_type typ
+              (Int.Set.add b
+                 (try Typehash.find state.by_type typ with
+                      Not_found -> Int.Set.empty));
+            b
 
 let add_equality state c s t=
   let i = add_term state s in
@@ -573,7 +573,7 @@ let is_redundant state id args =
     let prev_args = Identhash.find_all state.q_history id in
     List.exists
       (fun old_args ->
-	 Util.Array.for_all2 (fun i j -> Int.equal i (find state.uf j))
+         Util.Array.for_all2 (fun i j -> Int.equal i (find state.uf j))
          norm_args old_args)
       prev_args
     with Not_found -> false
@@ -591,26 +591,26 @@ let add_inst state (inst,int_subst) =
       let args = Array.map constr_of_term subst in
       let _ = Array.rev args in (* highest deBruijn index first *)
       let prf= mkApp(prfhead,args) in
-	  let s = inst_pattern subst inst.qe_lhs
-	  and t = inst_pattern subst inst.qe_rhs in
-	    state.changed<-true;
-	    state.rew_depth<-pred state.rew_depth;
-	    if inst.qe_pol then
-	      begin
-		debug (fun () ->
-		   (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++
+          let s = inst_pattern subst inst.qe_lhs
+          and t = inst_pattern subst inst.qe_rhs in
+            state.changed<-true;
+            state.rew_depth<-pred state.rew_depth;
+            if inst.qe_pol then
+              begin
+                debug (fun () ->
+                   (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++
                   (str "  [" ++ Printer.pr_econstr_env state.env state.sigma (EConstr.of_constr prf) ++ str " : " ++
                            pr_term state.env state.sigma s ++ str " == " ++ pr_term state.env state.sigma t ++ str "]"));
-		add_equality state prf s t
-	      end
-	    else
-	      begin
-		debug (fun () ->
-		   (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++
+                add_equality state prf s t
+              end
+            else
+              begin
+                debug (fun () ->
+                   (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++
                   (str "  [" ++ Printer.pr_econstr_env state.env state.sigma (EConstr.of_constr prf) ++ str " : " ++
                            pr_term state.env state.sigma s ++ str " <> " ++ pr_term state.env state.sigma t ++ str "]"));
-		add_disequality state (Hyp prf) s t
-	      end
+                add_disequality state (Hyp prf) s t
+              end
   end
 
 let link uf i j eq = (* links i -> j *)
@@ -643,8 +643,8 @@ let union state i1 i2 eq=
     link state.uf i1 i2 eq;
     Constrhash.replace state.by_type r1.class_type
       (Int.Set.remove i1
-	 (try Constrhash.find state.by_type r1.class_type with
-	      Not_found -> Int.Set.empty));
+         (try Constrhash.find state.by_type r1.class_type with
+              Not_found -> Int.Set.empty));
     let f= Int.Set.union r1.fathers r2.fathers in
       r2.weight<-Int.Set.cardinal f;
       r2.fathers<-f;
@@ -652,28 +652,28 @@ let union state i1 i2 eq=
       ST.delete_set state.sigtable r1.fathers;
       state.terms<-Int.Set.union state.terms r1.fathers;
       PacMap.iter
-	(fun pac b -> Queue.add (b,Cmark pac) state.marks)
-	state.uf.map.(i1).constructors;
+        (fun pac b -> Queue.add (b,Cmark pac) state.marks)
+        state.uf.map.(i1).constructors;
       PafMap.iter
-	(fun paf -> Int.Set.iter
-	   (fun b -> Queue.add (b,Fmark paf) state.marks))
-	r1.functions;
+        (fun paf -> Int.Set.iter
+           (fun b -> Queue.add (b,Fmark paf) state.marks))
+        r1.functions;
       match r1.inductive_status,r2.inductive_status with
-	  Unknown,_ -> ()
-	| Partial pac,Unknown ->
-	    r2.inductive_status<-Partial pac;
-	    state.pa_classes<-Int.Set.remove i1 state.pa_classes;
-	    state.pa_classes<-Int.Set.add i2 state.pa_classes
-	| Partial _ ,(Partial _ |Partial_applied) ->
-	    state.pa_classes<-Int.Set.remove i1 state.pa_classes
-	| Partial_applied,Unknown ->
-	    r2.inductive_status<-Partial_applied
-	| Partial_applied,Partial _ ->
-	    state.pa_classes<-Int.Set.remove i2 state.pa_classes;
-	    r2.inductive_status<-Partial_applied
-	| Total cpl,Unknown -> r2.inductive_status<-Total cpl;
-	| Total (i,pac),Total _ -> Queue.add (i,Cmark pac) state.marks
-	| _,_ -> ()
+          Unknown,_ -> ()
+        | Partial pac,Unknown ->
+            r2.inductive_status<-Partial pac;
+            state.pa_classes<-Int.Set.remove i1 state.pa_classes;
+            state.pa_classes<-Int.Set.add i2 state.pa_classes
+        | Partial _ ,(Partial _ |Partial_applied) ->
+            state.pa_classes<-Int.Set.remove i1 state.pa_classes
+        | Partial_applied,Unknown ->
+            r2.inductive_status<-Partial_applied
+        | Partial_applied,Partial _ ->
+            state.pa_classes<-Int.Set.remove i2 state.pa_classes;
+            r2.inductive_status<-Partial_applied
+        | Total cpl,Unknown -> r2.inductive_status<-Total cpl;
+        | Total (i,pac),Total _ -> Queue.add (i,Cmark pac) state.marks
+        | _,_ -> ()
 
 let merge eq state = (* merge and no-merge *)
   debug
@@ -684,9 +684,9 @@ let merge eq state = (* merge and no-merge *)
   and j=find uf eq.rhs in
     if not (Int.equal i j) then
       if (size uf i)<(size uf j) then
-	union state i j eq
+        union state i j eq
       else
-	union state j i (swap eq)
+        union state j i (swap eq)
 
 let update t state = (* update 1 and 2 *)
   debug
@@ -696,10 +696,10 @@ let update t state = (* update 1 and 2 *)
   let rep = get_representative state.uf i in
     begin
       match rep.inductive_status with
-	  Partial _ ->
-	    rep.inductive_status <- Partial_applied;
-	    state.pa_classes <- Int.Set.remove i state.pa_classes
-	| _ -> ()
+          Partial _ ->
+            rep.inductive_status <- Partial_applied;
+            state.pa_classes <- Int.Set.remove i state.pa_classes
+        | _ -> ()
     end;
     PacMap.iter
       (fun pac _ -> Queue.add (t,Cmark (append_pac v pac)) state.marks)
@@ -709,9 +709,9 @@ let update t state = (* update 1 and 2 *)
       rep.functions;
     try
       let s = ST.query sign state.sigtable in
-	Queue.add {lhs=t;rhs=s;rule=Congruence} state.combine
+        Queue.add {lhs=t;rhs=s;rule=Congruence} state.combine
     with
-	Not_found -> ST.enter t sign state.sigtable
+        Not_found -> ST.enter t sign state.sigtable
 
 let process_function_mark t rep paf state  =
   add_paf rep paf t;
@@ -720,35 +720,35 @@ let process_function_mark t rep paf state  =
 let process_constructor_mark t i rep pac state =
      add_pac state.uf.map.(i) pac t;
      match rep.inductive_status with
-	Total (s,opac) ->
-	  if not (Int.equal pac.cnode opac.cnode) then (* Conflict *)
-	    raise (Discriminable (s,opac,t,pac))
-	  else (* Match *)
-	    let cinfo = get_constructor_info state.uf pac.cnode in
-	    let rec f n oargs args=
-	      if n > 0 then
-		match (oargs,args) with
-		    s1::q1,s2::q2->
-		      Queue.add
-			{lhs=s1;rhs=s2;rule=Injection(s,opac,t,pac,n)}
-			state.combine;
-		      f (n-1) q1 q2
-		  | _-> anomaly ~label:"add_pacs"
-		      (Pp.str "weird error in injection subterms merge.")
-	    in f cinfo.ci_nhyps opac.args pac.args
+        Total (s,opac) ->
+          if not (Int.equal pac.cnode opac.cnode) then (* Conflict *)
+            raise (Discriminable (s,opac,t,pac))
+          else (* Match *)
+            let cinfo = get_constructor_info state.uf pac.cnode in
+            let rec f n oargs args=
+              if n > 0 then
+                match (oargs,args) with
+                    s1::q1,s2::q2->
+                      Queue.add
+                        {lhs=s1;rhs=s2;rule=Injection(s,opac,t,pac,n)}
+                        state.combine;
+                      f (n-1) q1 q2
+                  | _-> anomaly ~label:"add_pacs"
+                      (Pp.str "weird error in injection subterms merge.")
+            in f cinfo.ci_nhyps opac.args pac.args
       | Partial_applied | Partial _ ->
 (*	  add_pac state.uf.map.(i) pac t; *)
-	  state.terms<-Int.Set.union rep.lfathers state.terms
+          state.terms<-Int.Set.union rep.lfathers state.terms
       | Unknown ->
-	  if Int.equal pac.arity 0 then
-	    rep.inductive_status <- Total (t,pac)
-	  else
-	    begin
-	     (* add_pac state.uf.map.(i) pac t; *)
-	      state.terms<-Int.Set.union rep.lfathers state.terms;
-	      rep.inductive_status <- Partial pac;
-	      state.pa_classes<- Int.Set.add i state.pa_classes
-	    end
+          if Int.equal pac.arity 0 then
+            rep.inductive_status <- Total (t,pac)
+          else
+            begin
+             (* add_pac state.uf.map.(i) pac t; *)
+              state.terms<-Int.Set.union rep.lfathers state.terms;
+              rep.inductive_status <- Partial pac;
+              state.pa_classes<- Int.Set.add i state.pa_classes
+            end
 
 let process_mark t m state =
   debug
@@ -756,7 +756,7 @@ let process_mark t m state =
   let i=find state.uf t in
   let rep=get_representative state.uf i in
     match m with
-	Fmark paf -> process_function_mark t rep paf state
+        Fmark paf -> process_function_mark t rep paf state
       | Cmark pac -> process_constructor_mark t i rep pac state
 
 type explanation =
@@ -783,20 +783,20 @@ let check_disequalities state =
 let one_step state =
     try
       let eq = Queue.take state.combine in
-	merge eq state;
-	true
+        merge eq state;
+        true
     with Queue.Empty ->
       try
-	let (t,m) = Queue.take state.marks in
-	  process_mark t m state;
-	  true
+        let (t,m) = Queue.take state.marks in
+          process_mark t m state;
+          true
       with Queue.Empty ->
-	try
-	  let t = Int.Set.choose state.terms in
-	    state.terms<-Int.Set.remove t state.terms;
-	    update t state;
-	    true
-	with Not_found -> false
+        try
+          let t = Int.Set.choose state.terms in
+            state.terms<-Int.Set.remove t state.terms;
+            update t state;
+            true
+        with Not_found -> false
 
 let __eps__ = Id.of_string "_eps_"
 
@@ -810,21 +810,21 @@ let new_state_var typ state =
 let complete_one_class state i=
   match (get_representative state.uf i).inductive_status with
       Partial pac ->
-	let rec app t typ n =
-	  if n<=0 then t else
+        let rec app t typ n =
+          if n<=0 then t else
             let _,etyp,rest= destProd typ in
             let id = new_state_var (EConstr.of_constr etyp) state in
                 app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
         let _c = Typing.unsafe_type_of state.env state.sigma
-	  (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in
+          (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in
         let _c = EConstr.Unsafe.to_constr _c in
-	let _args =
-	  List.map (fun i -> constr_of_term (term state.uf  i))
-	    pac.args in
+        let _args =
+          List.map (fun i -> constr_of_term (term state.uf  i))
+            pac.args in
         let typ = Term.prod_applist _c (List.rev _args) in
-	let ct = app (term state.uf i) typ pac.arity in
-	  state.uf.epsilons <- pac :: state.uf.epsilons;
-	  ignore (add_term state ct)
+        let ct = app (term state.uf i) typ pac.arity in
+          state.uf.epsilons <- pac :: state.uf.epsilons;
+          ignore (add_term state ct)
     | _ -> anomaly (Pp.str "wrong incomplete class.")
 
 let complete state =
@@ -841,59 +841,59 @@ let make_fun_table state =
   Array.iteri
     (fun i inode -> if i < uf.size then
        match inode.clas with
-	   Rep rep ->
-	     PafMap.iter
-	       (fun paf _ ->
-		  let elem =
-		    try PafMap.find paf !funtab
-		    with Not_found -> Int.Set.empty in
-		    funtab:= PafMap.add paf (Int.Set.add i elem) !funtab)
-	       rep.functions
-	 | _ -> ()) state.uf.map;
+           Rep rep ->
+             PafMap.iter
+               (fun paf _ ->
+                  let elem =
+                    try PafMap.find paf !funtab
+                    with Not_found -> Int.Set.empty in
+                    funtab:= PafMap.add paf (Int.Set.add i elem) !funtab)
+               rep.functions
+         | _ -> ()) state.uf.map;
     !funtab
 
 
 let do_match state res pb_stack =
   let mp=Stack.pop pb_stack in
     match mp.mp_stack with
-	[] ->
-	  res:= (mp.mp_inst,mp.mp_subst) :: !res
+        [] ->
+          res:= (mp.mp_inst,mp.mp_subst) :: !res
       | (patt,cl)::remains ->
-	  let uf=state.uf in
-	    match patt with
-		PVar i ->
-		  if mp.mp_subst.(pred i)<0 then
-		    begin
-		      mp.mp_subst.(pred i)<- cl; (* no aliasing problem here *)
-		      Stack.push {mp with mp_stack=remains} pb_stack
-		    end
-		  else
-		    if Int.equal mp.mp_subst.(pred i) cl then
-		      Stack.push {mp with mp_stack=remains} pb_stack
-		    else (* mismatch for non-linear variable in pattern *) ()
-	      | PApp (f,[]) ->
-		  begin
-		    try let j=Termhash.find uf.syms f in
-		      if Int.equal (find uf j) cl then
-			Stack.push {mp with mp_stack=remains} pb_stack
-		    with Not_found -> ()
-		  end
-	      | PApp(f, ((last_arg::rem_args) as args)) ->
-		  try
-		    let j=Termhash.find uf.syms f in
-		    let paf={fsym=j;fnargs=List.length args} in
-		    let rep=get_representative uf cl in
-		    let good_terms = PafMap.find paf rep.functions in
-		    let aux i =
-		      let (s,t) = signature state.uf i in
-			Stack.push
-			  {mp with
-			     mp_subst=Array.copy mp.mp_subst;
-			     mp_stack=
-			      (PApp(f,rem_args),s) ::
-				(last_arg,t) :: remains} pb_stack in
-		      Int.Set.iter aux good_terms
-		  with Not_found -> ()
+          let uf=state.uf in
+            match patt with
+                PVar i ->
+                  if mp.mp_subst.(pred i)<0 then
+                    begin
+                      mp.mp_subst.(pred i)<- cl; (* no aliasing problem here *)
+                      Stack.push {mp with mp_stack=remains} pb_stack
+                    end
+                  else
+                    if Int.equal mp.mp_subst.(pred i) cl then
+                      Stack.push {mp with mp_stack=remains} pb_stack
+                    else (* mismatch for non-linear variable in pattern *) ()
+              | PApp (f,[]) ->
+                  begin
+                    try let j=Termhash.find uf.syms f in
+                      if Int.equal (find uf j) cl then
+                        Stack.push {mp with mp_stack=remains} pb_stack
+                    with Not_found -> ()
+                  end
+              | PApp(f, ((last_arg::rem_args) as args)) ->
+                  try
+                    let j=Termhash.find uf.syms f in
+                    let paf={fsym=j;fnargs=List.length args} in
+                    let rep=get_representative uf cl in
+                    let good_terms = PafMap.find paf rep.functions in
+                    let aux i =
+                      let (s,t) = signature state.uf i in
+                        Stack.push
+                          {mp with
+                             mp_subst=Array.copy mp.mp_subst;
+                             mp_stack=
+                              (PApp(f,rem_args),s) ::
+                                (last_arg,t) :: remains} pb_stack in
+                      Int.Set.iter aux good_terms
+                  with Not_found -> ()
 
 let paf_of_patt syms = function
     PVar _ -> invalid_arg "paf_of_patt: pattern is trivial"
@@ -908,49 +908,49 @@ let init_pb_stack state =
   let aux inst =
     begin
       let good_classes =
-	match inst.qe_lhs_valid with
-	  Creates_variables -> Int.Set.empty
-	| Normal ->
-	    begin
-	      try
-		let paf= paf_of_patt syms inst.qe_lhs in
-		  PafMap.find paf funtab
-	      with Not_found -> Int.Set.empty
-	    end
-	| Trivial typ ->
-	    begin
-	      try
-		Typehash.find state.by_type typ
-	      with Not_found -> Int.Set.empty
-	    end in
-	Int.Set.iter (fun i ->
-		       Stack.push
-			 {mp_subst = Array.make inst.qe_nvars (-1);
-			  mp_inst=inst;
-			  mp_stack=[inst.qe_lhs,i]} pb_stack) good_classes
+        match inst.qe_lhs_valid with
+          Creates_variables -> Int.Set.empty
+        | Normal ->
+            begin
+              try
+                let paf= paf_of_patt syms inst.qe_lhs in
+                  PafMap.find paf funtab
+              with Not_found -> Int.Set.empty
+            end
+        | Trivial typ ->
+            begin
+              try
+                Typehash.find state.by_type typ
+              with Not_found -> Int.Set.empty
+            end in
+        Int.Set.iter (fun i ->
+                       Stack.push
+                         {mp_subst = Array.make inst.qe_nvars (-1);
+                          mp_inst=inst;
+                          mp_stack=[inst.qe_lhs,i]} pb_stack) good_classes
     end;
     begin
       let good_classes =
-	match inst.qe_rhs_valid with
-	  Creates_variables -> Int.Set.empty
-	| Normal ->
-	    begin
-	      try
-		let paf= paf_of_patt syms inst.qe_rhs in
-		  PafMap.find paf funtab
-	      with Not_found -> Int.Set.empty
-	    end
-	| Trivial typ ->
-	    begin
-	      try
-		Typehash.find state.by_type typ
-	      with Not_found -> Int.Set.empty
-	    end in
-	Int.Set.iter (fun i ->
-		       Stack.push
-			 {mp_subst = Array.make inst.qe_nvars (-1);
-			  mp_inst=inst;
-			  mp_stack=[inst.qe_rhs,i]} pb_stack) good_classes
+        match inst.qe_rhs_valid with
+          Creates_variables -> Int.Set.empty
+        | Normal ->
+            begin
+              try
+                let paf= paf_of_patt syms inst.qe_rhs in
+                  PafMap.find paf funtab
+              with Not_found -> Int.Set.empty
+            end
+        | Trivial typ ->
+            begin
+              try
+                Typehash.find state.by_type typ
+              with Not_found -> Int.Set.empty
+            end in
+        Int.Set.iter (fun i ->
+                       Stack.push
+                         {mp_subst = Array.make inst.qe_nvars (-1);
+                          mp_inst=inst;
+                          mp_stack=[inst.qe_rhs,i]} pb_stack) good_classes
     end in
     List.iter aux state.quant;
     pb_stack
@@ -962,8 +962,8 @@ let find_instances state =
     debug (fun () -> str "Running E-matching algorithm ... ");
     try
       while true do
-	Control.check_for_interrupt ();
-	do_match state res pb_stack
+        Control.check_for_interrupt ();
+        do_match state res pb_stack
       done;
       anomaly (Pp.str "get out of here!")
     with Stack.Empty -> () in
@@ -977,37 +977,37 @@ let rec execute first_run state =
       one_step state do ()
     done;
     match check_disequalities state with
-	None ->
-	  if not(Int.Set.is_empty state.pa_classes) then
-	    begin
-	      debug (fun () -> str "First run was incomplete, completing ... ");
-	      complete state;
-	      execute false state
-	    end
-	  else
-	    if state.rew_depth>0 then
-	      let l=find_instances state in
-		List.iter (add_inst state) l;
-		if state.changed then
-		  begin
-		    state.changed <- false;
-		    execute true state
-		  end
-		else
-	      begin
-		debug (fun () -> str "Out of instances ... ");
-		None
-	      end
-	    else
-	      begin
-		debug (fun () -> str "Out of depth ... ");
-		None
-	      end
+        None ->
+          if not(Int.Set.is_empty state.pa_classes) then
+            begin
+              debug (fun () -> str "First run was incomplete, completing ... ");
+              complete state;
+              execute false state
+            end
+          else
+            if state.rew_depth>0 then
+              let l=find_instances state in
+                List.iter (add_inst state) l;
+                if state.changed then
+                  begin
+                    state.changed <- false;
+                    execute true state
+                  end
+                else
+              begin
+                debug (fun () -> str "Out of instances ... ");
+                None
+              end
+            else
+              begin
+                debug (fun () -> str "Out of depth ... ");
+                None
+              end
       | Some dis -> Some
-	  begin
-	    if first_run then Contradiction dis
-	    else Incomplete
-	  end
+          begin
+            if first_run then Contradiction dis
+            else Incomplete
+          end
   with Discriminable(s,spac,t,tpac) -> Some
     begin
       if first_run then Discrimination (s,spac,t,tpac)
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index f47a14cdc7..f82a55fe71 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -43,25 +43,25 @@ let rec ptrans p1 p3=
     | Trans(p1,p2), _ ->ptrans p1 (ptrans p2 p3)
     | Congr(p1,p2), Congr(p3,p4) ->pcongr (ptrans p1 p3) (ptrans p2 p4)
     | Congr(p1,p2), Trans({p_rule=Congr(p3,p4)},p5) ->
-	ptrans (pcongr (ptrans p1 p3) (ptrans p2 p4)) p5
+        ptrans (pcongr (ptrans p1 p3) (ptrans p2 p4)) p5
   | _, _ ->
       if term_equal p1.p_rhs p3.p_lhs then
-	{p_lhs=p1.p_lhs;
-	 p_rhs=p3.p_rhs;
-	 p_rule=Trans (p1,p3)}
+        {p_lhs=p1.p_lhs;
+         p_rhs=p3.p_rhs;
+         p_rule=Trans (p1,p3)}
       else anomaly (Pp.str "invalid cc transitivity.")
 
 let rec psym p =
   match p.p_rule with
       Refl _ -> p
     | SymAx s ->
-	{p_lhs=p.p_rhs;
-	 p_rhs=p.p_lhs;
-	 p_rule=Ax s}
+        {p_lhs=p.p_rhs;
+         p_rhs=p.p_lhs;
+         p_rule=Ax s}
     | Ax s->
-	{p_lhs=p.p_rhs;
-	 p_rhs=p.p_lhs;
-	 p_rule=SymAx s}
+        {p_lhs=p.p_rhs;
+         p_rhs=p.p_lhs;
+         p_rule=SymAx s}
   | Inject (p0,c,n,a)->
       {p_lhs=p.p_rhs;
        p_rhs=p.p_lhs;
@@ -84,9 +84,9 @@ let psymax axioms s =
 let rec nth_arg t n=
   match t with
       Appli (t1,t2)->
-	if n>0 then
-	  nth_arg t1 (n-1)
-	else t2
+        if n>0 then
+          nth_arg t1 (n-1)
+        else t2
     | _ -> anomaly ~label:"nth_arg" (Pp.str "not enough args.")
 
 let pinject p c n a =
@@ -99,7 +99,7 @@ let rec equal_proof env sigma uf i j=
   if i=j then prefl (term uf i) else
     let (li,lj)=join_path uf i j in
     ptrans (path_proof env sigma uf i li) (psym (path_proof env sigma uf j lj))
-      
+
 and edge_proof env sigma uf ((i,j),eq)=
   debug (fun () -> str "edge_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
   let pi=equal_proof env sigma uf i eq.lhs in
@@ -107,15 +107,15 @@ and edge_proof env sigma uf ((i,j),eq)=
   let pij=
     match eq.rule with
       Axiom (s,reversed)->
-	if reversed then psymax (axioms uf) s
-	else pax (axioms uf) s
+        if reversed then psymax (axioms uf) s
+        else pax (axioms uf) s
     | Congruence ->congr_proof env sigma uf eq.lhs eq.rhs
-    | Injection (ti,ipac,tj,jpac,k) -> (* pi_k ipac = p_k jpac *) 
+    | Injection (ti,ipac,tj,jpac,k) -> (* pi_k ipac = p_k jpac *)
       let p=ind_proof env sigma uf ti ipac tj jpac in
       let cinfo= get_constructor_info uf ipac.cnode in
-      pinject p cinfo.ci_constr cinfo.ci_nhyps k in  
+      pinject p cinfo.ci_constr cinfo.ci_nhyps k in
   ptrans (ptrans pi pij) pj
-  
+
 and constr_proof env sigma uf i ipac=
   debug (fun () -> str "constr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20));
   let t=find_oldest_pac uf i ipac in
@@ -128,20 +128,20 @@ and constr_proof env sigma uf i ipac=
     let targ=term uf arg in
     let p=constr_proof env sigma uf fi fipac in
     ptrans eq_it (pcongr p (prefl targ))
-      
+
 and path_proof env sigma uf i l=
   debug (fun () -> str "path_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ str "{" ++
-	   (prlist_with_sep (fun () -> str ",") (fun ((_,j),_) -> int j) l) ++ str "}");
+           (prlist_with_sep (fun () -> str ",") (fun ((_,j),_) -> int j) l) ++ str "}");
   match l with
   | [] -> prefl (term uf i)
   | x::q->ptrans (path_proof env sigma uf (snd (fst x)) q) (edge_proof env sigma uf x)
-    
+
 and congr_proof env sigma uf i j=
   debug (fun () -> str "congr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
   let (i1,i2) = subterms uf i
   and (j1,j2) = subterms uf j in
   pcongr (equal_proof env sigma uf i1 j1) (equal_proof env sigma uf i2 j2)
-    
+
 and ind_proof env sigma uf i ipac j jpac=
    debug (fun () -> str "ind_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
   let p=equal_proof env sigma uf i j
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index b5be1cdd89..556e6b48e6 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -51,40 +51,40 @@ let sf_of env sigma c = snd (sort_of env sigma c)
 let rec decompose_term env sigma t=
     match EConstr.kind sigma (whd env sigma t) with
       App (f,args)->
-	let tf=decompose_term env sigma f in
-	let targs=Array.map (decompose_term env sigma) args in
-	  Array.fold_left (fun s t->Appli (s,t)) tf targs
+        let tf=decompose_term env sigma f in
+        let targs=Array.map (decompose_term env sigma) args in
+          Array.fold_left (fun s t->Appli (s,t)) tf targs
     | Prod (_,a,_b) when noccurn sigma 1 _b ->
-	let b = Termops.pop _b in
-	let sort_b = sf_of env sigma b in
-	let sort_a = sf_of env sigma a in
-	Appli(Appli(Product (sort_a,sort_b) ,
-		    decompose_term env sigma a),
-	      decompose_term env sigma b)
+        let b = Termops.pop _b in
+        let sort_b = sf_of env sigma b in
+        let sort_a = sf_of env sigma a in
+        Appli(Appli(Product (sort_a,sort_b) ,
+                    decompose_term env sigma a),
+              decompose_term env sigma b)
     | Construct c ->
-	let (((mind,i_ind),i_con),u)= c in 
-	let u = EInstance.kind sigma u in
-	let canon_mind = MutInd.make1 (MutInd.canonical mind) in
-	let canon_ind = canon_mind,i_ind in
-	let (oib,_)=Global.lookup_inductive (canon_ind) in
+        let (((mind,i_ind),i_con),u)= c in
+        let u = EInstance.kind sigma u in
+        let canon_mind = MutInd.make1 (MutInd.canonical mind) in
+        let canon_ind = canon_mind,i_ind in
+        let (oib,_)=Global.lookup_inductive (canon_ind) in
         let nargs=constructor_nallargs env (canon_ind,i_con) in
-	  Constructor {ci_constr= ((canon_ind,i_con),u);
-		       ci_arity=nargs;
-		       ci_nhyps=nargs-oib.mind_nparams}
-    | Ind c -> 
-	let (mind,i_ind),u = c in 
-	let u = EInstance.kind sigma u in
-	let canon_mind = MutInd.make1 (MutInd.canonical mind) in
-	let canon_ind = canon_mind,i_ind in  (Symb (Constr.mkIndU (canon_ind,u)))
-    | Const (c,u) -> 
-	let u = EInstance.kind sigma u in
-	let canon_const = Constant.make1 (Constant.canonical c) in 
-	  (Symb (Constr.mkConstU (canon_const,u)))
-    | Proj (p, c) -> 
+          Constructor {ci_constr= ((canon_ind,i_con),u);
+                       ci_arity=nargs;
+                       ci_nhyps=nargs-oib.mind_nparams}
+    | Ind c ->
+        let (mind,i_ind),u = c in
+        let u = EInstance.kind sigma u in
+        let canon_mind = MutInd.make1 (MutInd.canonical mind) in
+        let canon_ind = canon_mind,i_ind in  (Symb (Constr.mkIndU (canon_ind,u)))
+    | Const (c,u) ->
+        let u = EInstance.kind sigma u in
+        let canon_const = Constant.make1 (Constant.canonical c) in
+          (Symb (Constr.mkConstU (canon_const,u)))
+    | Proj (p, c) ->
         let canon_mind kn = MutInd.make1 (MutInd.canonical kn) in
         let p' = Projection.map canon_mind p in
-	let c = Retyping.expand_projection env sigma p' c [] in
-	decompose_term env sigma c
+        let c = Retyping.expand_projection env sigma p' c [] in
+        decompose_term env sigma c
     | _ ->
        let t = Termops.strip_outer_cast sigma t in
        if closed0 sigma t then Symb (EConstr.to_constr ~abort_on_undefined_evars:false sigma t) else raise Not_found
@@ -97,33 +97,33 @@ let atom_of_constr env sigma term =
   let kot = EConstr.kind sigma wh in
     match kot with
       App (f,args)->
-	if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3
-	  then `Eq (args.(0),
-		   decompose_term env sigma args.(1),
-		   decompose_term env sigma args.(2))
-	  else `Other (decompose_term env sigma term)
+        if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3
+          then `Eq (args.(0),
+                   decompose_term env sigma args.(1),
+                   decompose_term env sigma args.(2))
+          else `Other (decompose_term env sigma term)
     | _ -> `Other (decompose_term env sigma term)
 
 let rec pattern_of_constr env sigma c =
   match EConstr.kind sigma (whd env sigma c) with
       App (f,args)->
-	let pf = decompose_term env sigma f in
-	let pargs,lrels = List.split
-	  (Array.map_to_list (pattern_of_constr env sigma) args) in
-	  PApp (pf,List.rev pargs),
-	List.fold_left Int.Set.union Int.Set.empty lrels
+        let pf = decompose_term env sigma f in
+        let pargs,lrels = List.split
+          (Array.map_to_list (pattern_of_constr env sigma) args) in
+          PApp (pf,List.rev pargs),
+        List.fold_left Int.Set.union Int.Set.empty lrels
     | Prod (_,a,_b) when noccurn sigma 1 _b ->
-	let b = Termops.pop _b in
-	let pa,sa = pattern_of_constr env sigma a in
-	let pb,sb = pattern_of_constr env sigma b in
-	let sort_b = sf_of env sigma b in
-	let sort_a = sf_of env sigma a in
-	  PApp(Product (sort_a,sort_b),
-	       [pa;pb]),(Int.Set.union sa sb)
+        let b = Termops.pop _b in
+        let pa,sa = pattern_of_constr env sigma a in
+        let pb,sb = pattern_of_constr env sigma b in
+        let sort_b = sf_of env sigma b in
+        let sort_a = sf_of env sigma a in
+          PApp(Product (sort_a,sort_b),
+               [pa;pb]),(Int.Set.union sa sb)
     | Rel i -> PVar i,Int.Set.singleton i
     | _ ->
-	let pf = decompose_term env sigma c in
-	  PApp (pf,[]),Int.Set.empty
+        let pf = decompose_term env sigma c in
+          PApp (pf,[]),Int.Set.empty
 
 let non_trivial = function
     PVar _ -> false
@@ -132,52 +132,52 @@ let non_trivial = function
 let patterns_of_constr env sigma nrels term=
   let f,args=
     try destApp sigma (whd_delta env sigma term) with DestKO -> raise Not_found in
-	if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3
-	then
-	  let patt1,rels1 = pattern_of_constr env sigma args.(1)
-	  and patt2,rels2 = pattern_of_constr env sigma args.(2) in
-	  let valid1 =
-	    if not (Int.equal (Int.Set.cardinal rels1) nrels) then Creates_variables
-	    else if non_trivial patt1 then Normal
-	    else Trivial (EConstr.to_constr sigma args.(0))
-	  and valid2 =
-	    if not (Int.equal (Int.Set.cardinal rels2) nrels) then Creates_variables
-	    else if non_trivial patt2 then Normal
-	    else Trivial (EConstr.to_constr sigma args.(0)) in
-	    if valid1 != Creates_variables
-	      || valid2 != Creates_variables  then
-	      nrels,valid1,patt1,valid2,patt2
-	    else raise Not_found
-	else raise Not_found
+        if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3
+        then
+          let patt1,rels1 = pattern_of_constr env sigma args.(1)
+          and patt2,rels2 = pattern_of_constr env sigma args.(2) in
+          let valid1 =
+            if not (Int.equal (Int.Set.cardinal rels1) nrels) then Creates_variables
+            else if non_trivial patt1 then Normal
+            else Trivial (EConstr.to_constr sigma args.(0))
+          and valid2 =
+            if not (Int.equal (Int.Set.cardinal rels2) nrels) then Creates_variables
+            else if non_trivial patt2 then Normal
+            else Trivial (EConstr.to_constr sigma args.(0)) in
+            if valid1 != Creates_variables
+              || valid2 != Creates_variables  then
+              nrels,valid1,patt1,valid2,patt2
+            else raise Not_found
+        else raise Not_found
 
 let rec quantified_atom_of_constr env sigma nrels term =
   match EConstr.kind sigma (whd_delta env sigma term) with
       Prod (id,atom,ff) ->
-	if is_global sigma (Lazy.force _False) ff then
-	  let patts=patterns_of_constr env sigma nrels atom in
-	      `Nrule patts
-	else 
+        if is_global sigma (Lazy.force _False) ff then
+          let patts=patterns_of_constr env sigma nrels atom in
+              `Nrule patts
+        else
           quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma (succ nrels) ff
-    | _ ->  
-	let patts=patterns_of_constr env sigma nrels term in
-	    `Rule patts
+    | _ ->
+        let patts=patterns_of_constr env sigma nrels term in
+            `Rule patts
 
 let litteral_of_constr env sigma term=
   match EConstr.kind sigma (whd_delta env sigma term) with
     | Prod (id,atom,ff) ->
-	if is_global sigma (Lazy.force _False) ff then
-	  match (atom_of_constr env sigma atom) with
-	      `Eq(t,a,b) -> `Neq(t,a,b)
-	    | `Other(p) -> `Nother(p)
-	else
-	  begin
-	    try 
+        if is_global sigma (Lazy.force _False) ff then
+          match (atom_of_constr env sigma atom) with
+              `Eq(t,a,b) -> `Neq(t,a,b)
+            | `Other(p) -> `Nother(p)
+        else
+          begin
+            try
               quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma 1 ff
-	    with Not_found ->
-	      `Other (decompose_term env sigma term)
-	  end
+            with Not_found ->
+              `Other (decompose_term env sigma term)
+          end
     | _ ->
-	atom_of_constr env sigma term
+        atom_of_constr env sigma term
 
 
 (* store all equalities from the context *)
@@ -191,38 +191,38 @@ let make_prb gls depth additionnal_terms =
   let neg_hyps =ref [] in
     List.iter
       (fun c ->
-	 let t = decompose_term env sigma c in
-	   ignore (add_term state t)) additionnal_terms;
+         let t = decompose_term env sigma c in
+           ignore (add_term state t)) additionnal_terms;
     List.iter
       (fun decl ->
          let id = NamedDecl.get_id decl in
-	 begin
-	   let cid=Constr.mkVar id in
-	   match litteral_of_constr env sigma (NamedDecl.get_type decl) with
-	       `Eq (t,a,b) -> add_equality state cid a b
-	     | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b
-	     | `Other ph ->
-		 List.iter
-		   (fun (cidn,nh) ->
-		      add_disequality state (HeqnH (cid,cidn)) ph nh)
-		   !neg_hyps;
-		 pos_hyps:=(cid,ph):: !pos_hyps
-	     | `Nother nh ->
-		 List.iter
-		   (fun (cidp,ph) ->
-		      add_disequality state (HeqnH (cidp,cid)) ph nh)
-		   !pos_hyps;
-		 neg_hyps:=(cid,nh):: !neg_hyps
-	     | `Rule patts -> add_quant state id true patts
-	     | `Nrule patts -> add_quant state id false patts
-	 end) (Proofview.Goal.hyps gls);
+         begin
+           let cid=Constr.mkVar id in
+           match litteral_of_constr env sigma (NamedDecl.get_type decl) with
+               `Eq (t,a,b) -> add_equality state cid a b
+             | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b
+             | `Other ph ->
+                 List.iter
+                   (fun (cidn,nh) ->
+                      add_disequality state (HeqnH (cid,cidn)) ph nh)
+                   !neg_hyps;
+                 pos_hyps:=(cid,ph):: !pos_hyps
+             | `Nother nh ->
+                 List.iter
+                   (fun (cidp,ph) ->
+                      add_disequality state (HeqnH (cidp,cid)) ph nh)
+                   !pos_hyps;
+                 neg_hyps:=(cid,nh):: !neg_hyps
+             | `Rule patts -> add_quant state id true patts
+             | `Nrule patts -> add_quant state id false patts
+         end) (Proofview.Goal.hyps gls);
     begin
       match atom_of_constr env sigma (pf_concl gls) with
-	  `Eq (t,a,b) -> add_disequality state Goal a b
-	|	`Other g ->
-		  List.iter
-	      (fun (idp,ph) ->
-		 add_disequality state (HeqG idp) ph g) !pos_hyps
+          `Eq (t,a,b) -> add_disequality state Goal a b
+        |	`Other g ->
+                  List.iter
+              (fun (idp,ph) ->
+                 add_disequality state (HeqG idp) ph g) !pos_hyps
     end;
     state
 
@@ -275,7 +275,7 @@ let assert_before n c =
 
 let refresh_type env evm ty =
   Evarsolve.refresh_universes ~status:Evd.univ_flexible ~refreshset:true
-			      (Some false) env evm ty
+                              (Some false) env evm ty
 
 let refresh_universes ty k =
   Proofview.Goal.enter begin fun gl ->
@@ -295,60 +295,60 @@ let rec proof_tac p : unit Proofview.tactic =
       Ax c -> exact_check (EConstr.of_constr c)
     | SymAx c ->
         let c = EConstr.of_constr c in
-	let l=constr_of_term p.p_lhs and
-	    r=constr_of_term p.p_rhs in
-	refresh_universes (type_of l) (fun typ ->
+        let l=constr_of_term p.p_lhs and
+            r=constr_of_term p.p_rhs in
+        refresh_universes (type_of l) (fun typ ->
         app_global _sym_eq [|typ;r;l;c|] exact_check)
     | Refl t ->
-	let lr = constr_of_term t in
-	refresh_universes (type_of lr) (fun typ ->
+        let lr = constr_of_term t in
+        refresh_universes (type_of lr) (fun typ ->
         app_global _refl_equal [|typ;constr_of_term t|] exact_check)
     | Trans (p1,p2)->
-	let t1 = constr_of_term p1.p_lhs and
-	    t2 = constr_of_term p1.p_rhs and
-	    t3 = constr_of_term p2.p_rhs in
-	refresh_universes (type_of t2) (fun typ ->
-	let prf = app_global_with_holes _trans_eq [|typ;t1;t2;t3;|] 2 in
+        let t1 = constr_of_term p1.p_lhs and
+            t2 = constr_of_term p1.p_rhs and
+            t3 = constr_of_term p2.p_rhs in
+        refresh_universes (type_of t2) (fun typ ->
+        let prf = app_global_with_holes _trans_eq [|typ;t1;t2;t3;|] 2 in
           Tacticals.New.tclTHENS prf [(proof_tac p1);(proof_tac p2)])
     | Congr (p1,p2)->
-	let tf1=constr_of_term p1.p_lhs
-	and tx1=constr_of_term p2.p_lhs
-	and tf2=constr_of_term p1.p_rhs
-	and tx2=constr_of_term p2.p_rhs in
-	refresh_universes (type_of tf1) (fun typf ->
-	refresh_universes (type_of tx1) (fun typx ->
-	refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx ->
+        let tf1=constr_of_term p1.p_lhs
+        and tx1=constr_of_term p2.p_lhs
+        and tf2=constr_of_term p1.p_rhs
+        and tx2=constr_of_term p2.p_rhs in
+        refresh_universes (type_of tf1) (fun typf ->
+        refresh_universes (type_of tx1) (fun typx ->
+        refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx ->
         let id = Tacmach.New.pf_get_new_id (Id.of_string "f") gl in
         let appx1 = mkLambda(make_annot (Name id) Sorts.Relevant,typf,mkApp(mkRel 1,[|tx1|])) in
-	let lemma1 = app_global_with_holes _f_equal [|typf;typfx;appx1;tf1;tf2|] 1 in
-	let lemma2 = app_global_with_holes _f_equal [|typx;typfx;tf2;tx1;tx2|] 1 in
-	let prf =
-	  app_global_with_holes _trans_eq
-		[|typfx;
-		  mkApp(tf1,[|tx1|]);
-		  mkApp(tf2,[|tx1|]);
-		  mkApp(tf2,[|tx2|])|] 2 in
-	  Tacticals.New.tclTHENS prf
-	    [Tacticals.New.tclTHEN lemma1 (proof_tac p1);
-  	     Tacticals.New.tclFIRST
-	       [Tacticals.New.tclTHEN lemma2 (proof_tac p2);
-		reflexivity;
+        let lemma1 = app_global_with_holes _f_equal [|typf;typfx;appx1;tf1;tf2|] 1 in
+        let lemma2 = app_global_with_holes _f_equal [|typx;typfx;tf2;tx1;tx2|] 1 in
+        let prf =
+          app_global_with_holes _trans_eq
+                [|typfx;
+                  mkApp(tf1,[|tx1|]);
+                  mkApp(tf2,[|tx1|]);
+                  mkApp(tf2,[|tx2|])|] 2 in
+          Tacticals.New.tclTHENS prf
+            [Tacticals.New.tclTHEN lemma1 (proof_tac p1);
+             Tacticals.New.tclFIRST
+               [Tacticals.New.tclTHEN lemma2 (proof_tac p2);
+                reflexivity;
                 Tacticals.New.tclZEROMSG
-		    (Pp.str
-		       "I don't know how to handle dependent equality")]])))
+                    (Pp.str
+                       "I don't know how to handle dependent equality")]])))
   | Inject (prf,cstr,nargs,argind) ->
-	 let ti=constr_of_term prf.p_lhs in
-	 let tj=constr_of_term prf.p_rhs in
-	 let default=constr_of_term p.p_lhs in
-	 let special=mkRel (1+nargs-argind) in
-	 refresh_universes (type_of ti) (fun intype ->
+         let ti=constr_of_term prf.p_lhs in
+         let tj=constr_of_term prf.p_rhs in
+         let default=constr_of_term p.p_lhs in
+         let special=mkRel (1+nargs-argind) in
+         refresh_universes (type_of ti) (fun intype ->
          refresh_universes (type_of default) (fun outtype ->
          let sigma, proj =
            build_projection intype cstr special default gl
          in
-	 let injt=
+         let injt=
            app_global_with_holes _f_equal [|intype;outtype;proj;ti;tj|] 1 in
-	 Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+         Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
                                (Tacticals.New.tclTHEN injt (proof_tac prf))))
   with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end
@@ -371,7 +371,7 @@ let refine_exact_check c =
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm) (exact_check c)
   end
 
-let convert_to_goal_tac c t1 t2 p = 
+let convert_to_goal_tac c t1 t2 p =
   Proofview.Goal.enter begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
   let k sort =
@@ -381,7 +381,7 @@ let convert_to_goal_tac c t1 t2 p =
     let identity=mkLambda (make_annot (Name x) Sorts.Relevant,sort,mkRel 1) in
     let endt = app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name e)))
-			   [proof_tac p; endt refine_exact_check]
+                           [proof_tac p; endt refine_exact_check]
   in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k
   end
 
@@ -405,7 +405,7 @@ let discriminate_tac cstru p =
     let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in
     let neweq=app_global _eq [|intype;lhs;rhs|] in
     Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm)
-			  (Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
+                          (Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
       [proof_tac p; Equality.discrHyp hid])
   end
 
@@ -430,13 +430,13 @@ let cc_tactic depth additionnal_terms =
     match sol with
       None -> Tacticals.New.tclFAIL 0 (str "congruence failed")
     | Some reason ->
-	debug (fun () -> Pp.str "Goal solved, generating proof ...");
-	match reason with
-	  Discrimination (i,ipac,j,jpac) ->
+        debug (fun () -> Pp.str "Goal solved, generating proof ...");
+        match reason with
+          Discrimination (i,ipac,j,jpac) ->
             let p=build_proof (Tacmach.New.pf_env gl) sigma uf (`Discr (i,ipac,j,jpac)) in
-	    let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
-	    discriminate_tac cstr p
-	| Incomplete ->
+            let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
+            discriminate_tac cstr p
+        | Incomplete ->
       let open Glob_term in
       let env = Proofview.Goal.env gl in
       let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in
@@ -456,20 +456,20 @@ let cc_tactic depth additionnal_terms =
                     end ++
                     str "  replacing metavariables by arbitrary terms.") in
       Tacticals.New.tclFAIL 0 msg
-	| Contradiction dis ->
+        | Contradiction dis ->
       let env = Proofview.Goal.env gl in
             let p=build_proof env sigma uf (`Prove (dis.lhs,dis.rhs)) in
-	    let ta=term uf dis.lhs and tb=term uf dis.rhs in
-	    match dis.rule with
-	      Goal -> proof_tac p
-	    | Hyp id -> refute_tac (EConstr.of_constr id) ta tb p
-	    | HeqG id ->
+            let ta=term uf dis.lhs and tb=term uf dis.rhs in
+            match dis.rule with
+              Goal -> proof_tac p
+            | Hyp id -> refute_tac (EConstr.of_constr id) ta tb p
+            | HeqG id ->
                 let id = EConstr.of_constr id in
-		convert_to_goal_tac id ta tb p
-	    | HeqnH (ida,idb) ->
+                convert_to_goal_tac id ta tb p
+            | HeqnH (ida,idb) ->
                 let ida = EConstr.of_constr ida in
                 let idb = EConstr.of_constr idb in
-		convert_to_hyp_tac ida ta idb tb p
+                convert_to_hyp_tac ida ta idb tb p
   end
 
 let cc_fail =
@@ -509,21 +509,21 @@ let f_equal =
     let cut_eq c1 c2 =
       try (* type_of can raise an exception *)
         Tacticals.New.tclTHENS
-	  (mk_eq _eq c1 c2 Tactics.cut)
-	  [Proofview.tclUNIT ();Tacticals.New.tclTRY ((app_global _refl_equal [||]) apply)]
+          (mk_eq _eq c1 c2 Tactics.cut)
+          [Proofview.tclUNIT ();Tacticals.New.tclTRY ((app_global _refl_equal [||]) apply)]
       with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
     in
     Proofview.tclORELSE
       begin match EConstr.kind sigma concl with
       | App (r,[|_;t;t'|]) when is_global sigma (Lazy.force _eq) r ->
-	  begin match EConstr.kind sigma t, EConstr.kind sigma t' with
-	  | App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') ->
-	      let rec cuts i =
-		if i < 0 then Tacticals.New.tclTRY (congruence_tac 1000 [])
-		else Tacticals.New.tclTHENFIRST (cut_eq v.(i) v'.(i)) (cuts (i-1))
-	      in cuts (Array.length v - 1)
-	  | _ -> Proofview.tclUNIT ()
-	  end
+          begin match EConstr.kind sigma t, EConstr.kind sigma t' with
+          | App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') ->
+              let rec cuts i =
+                if i < 0 then Tacticals.New.tclTRY (congruence_tac 1000 [])
+                else Tacticals.New.tclTHENFIRST (cut_eq v.(i) v'.(i)) (cuts (i-1))
+              in cuts (Array.length v - 1)
+          | _ -> Proofview.tclUNIT ()
+          end
       | _ -> Proofview.tclUNIT ()
       end
       begin function (e, info) -> match e with