[funind] Untabify; necessary to ease the review of subsequent work.

1 files changed, 425 insertions, 425 deletions

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 857b7df96f..376e1cb2cc 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -56,7 +56,7 @@ let do_observe_tac s tac g =
     let reraise = CErrors.push reraise in
     let e = ExplainErr.process_vernac_interp_error reraise in
     observe (hov 0 (str "observation "++ s++str " raised exception " ++
-	     CErrors.iprint e ++ str " on goal" ++ fnl() ++ goal ));
+             CErrors.iprint e ++ str " on goal" ++ fnl() ++ goal ));
     iraise reraise;;
 
 let observe_tac s tac g =
@@ -115,8 +115,8 @@ let generate_type evd g_to_f f graph i =
   in
   (*i We need to name the vars [res] and [fv] i*)
   let filter = fun decl -> match RelDecl.get_name decl with
-			   | Name id -> Some id
-			   | Anonymous -> None
+                           | Name id -> Some id
+                           | Anonymous -> None
   in
   let named_ctxt = Id.Set.of_list (List.map_filter filter fun_ctxt) in
   let res_id = Namegen.next_ident_away_in_goal (Id.of_string "_res") named_ctxt in
@@ -232,12 +232,12 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
     (* and built the intro pattern for each of them *)
     let intro_pats =
       List.map
-	(fun decl ->
-	   List.map
+        (fun decl ->
+           List.map
              (fun id -> CAst.make @@ IntroNaming (Namegen.IntroIdentifier id))
-	     (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl)))))
-	)
-	branches
+             (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl)))))
+        )
+        branches
     in
     (* before building the full intro pattern for the principle *)
     let eq_ind = make_eq () in
@@ -249,113 +249,113 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
     let prove_branche i g =
       (* We get the identifiers of this branch *)
       let pre_args =
-      	List.fold_right
+        List.fold_right
           (fun {CAst.v=pat} acc ->
-      	     match pat with
+             match pat with
                | IntroNaming (Namegen.IntroIdentifier id) -> id::acc
-      	       | _ -> anomaly (Pp.str "Not an identifier.")
-      	  )
-      	  (List.nth intro_pats (pred i))
-      	  []
+               | _ -> anomaly (Pp.str "Not an identifier.")
+          )
+          (List.nth intro_pats (pred i))
+          []
       in
       (* and get the real args of the branch by unfolding the defined constant *)
       (*
-	 We can then recompute the arguments of the constructor.
-	 For each [hid] introduced by this branch, if [hid] has type
-	 $forall res, res=fv -> graph.(j)\ x_1\ x_n res$ the corresponding arguments of the constructor are
-	 [ fv (hid fv (refl_equal fv)) ].
-	 If [hid] has another type the corresponding argument of the constructor is [hid]
+         We can then recompute the arguments of the constructor.
+         For each [hid] introduced by this branch, if [hid] has type
+         $forall res, res=fv -> graph.(j)\ x_1\ x_n res$ the corresponding arguments of the constructor are
+         [ fv (hid fv (refl_equal fv)) ].
+         If [hid] has another type the corresponding argument of the constructor is [hid]
       *)
       let constructor_args g =
-	List.fold_right 
-	  (fun hid acc ->
-	     let type_of_hid = pf_unsafe_type_of g (mkVar hid) in
-	     let sigma = project g in
-	     match EConstr.kind sigma type_of_hid with
+        List.fold_right
+          (fun hid acc ->
+             let type_of_hid = pf_unsafe_type_of g (mkVar hid) in
+             let sigma = project g in
+             match EConstr.kind sigma type_of_hid with
                | Prod(_,_,t') ->
-		   begin
-		     match EConstr.kind sigma t' with
+                   begin
+                     match EConstr.kind sigma t' with
                        | Prod(_,t'',t''') ->
-			   begin
-			     match EConstr.kind sigma t'',EConstr.kind sigma t''' with
-			       | App(eq,args), App(graph',_)
-				   when
-				     (EConstr.eq_constr sigma eq eq_ind) &&
-				       Array.exists  (EConstr.eq_constr_nounivs sigma graph') graphs_constr ->
-				   (args.(2)::(mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|]))
-				    ::acc)
-			       | _ -> mkVar hid ::  acc
-			   end
-		       | _ -> mkVar hid :: acc
-		   end
-	       | _ -> mkVar hid :: acc
-	  ) pre_args []
+                           begin
+                             match EConstr.kind sigma t'',EConstr.kind sigma t''' with
+                               | App(eq,args), App(graph',_)
+                                   when
+                                     (EConstr.eq_constr sigma eq eq_ind) &&
+                                       Array.exists  (EConstr.eq_constr_nounivs sigma graph') graphs_constr ->
+                                   (args.(2)::(mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|]))
+                                    ::acc)
+                               | _ -> mkVar hid ::  acc
+                           end
+                       | _ -> mkVar hid :: acc
+                   end
+               | _ -> mkVar hid :: acc
+          ) pre_args []
       in
       (* in fact we must also add the parameters to the constructor args *)
       let constructor_args g =
-	let params_id = fst (List.chop princ_infos.nparams args_names) in
-	(List.map mkVar params_id)@((constructor_args g))
+        let params_id = fst (List.chop princ_infos.nparams args_names) in
+        (List.map mkVar params_id)@((constructor_args g))
       in
       (* We then get the constructor corresponding to this branch and
-	 modifies the references has needed i.e.
-	 if the constructor is the last one of the current inductive then
-	 add one the number of the inductive to take and add the number of constructor of the previous
-	 graph to the minimal constructor number
+         modifies the references has needed i.e.
+         if the constructor is the last one of the current inductive then
+         add one the number of the inductive to take and add the number of constructor of the previous
+         graph to the minimal constructor number
       *)
       let constructor =
-	let constructor_num = i - !min_constr_number in
-	let length = Array.length (mib.Declarations.mind_packets.(!ind_number).Declarations.mind_consnames) in
-	if constructor_num <= length
-	then
-	  begin
-	    (kn,!ind_number),constructor_num
-	  end
-	else
-	  begin
-	    incr ind_number;
-	    min_constr_number := !min_constr_number + length ;
-	    (kn,!ind_number),1
-	  end
+        let constructor_num = i - !min_constr_number in
+        let length = Array.length (mib.Declarations.mind_packets.(!ind_number).Declarations.mind_consnames) in
+        if constructor_num <= length
+        then
+          begin
+            (kn,!ind_number),constructor_num
+          end
+        else
+          begin
+            incr ind_number;
+            min_constr_number := !min_constr_number + length ;
+            (kn,!ind_number),1
+          end
       in
       (* we can then build the final proof term *)
       let app_constructor g = applist((mkConstructU(constructor,u)),constructor_args g) in
       (* an apply the tactic *)
       let res,hres =
-	match generate_fresh_id (Id.of_string "z") (ids(* @this_branche_ids *)) 2 with
-	  | [res;hres] -> res,hres
-	  | _ -> assert false
+        match generate_fresh_id (Id.of_string "z") (ids(* @this_branche_ids *)) 2 with
+          | [res;hres] -> res,hres
+          | _ -> assert false
       in
       (* observe (str "constructor := " ++ Printer.pr_lconstr_env (pf_env g) app_constructor); *)
       (
-	tclTHENLIST
-	  [
-	    observe_tac("h_intro_patterns ")  (let l = (List.nth intro_pats (pred i)) in 
-					       match l with 
-						 | [] -> tclIDTAC 
-						 | _ -> Proofview.V82.of_tactic (intro_patterns false l));
-	    (* unfolding of all the defined variables introduced by this branch *)
-	    (* observe_tac "unfolding" pre_tac; *)
-	    (* $zeta$ normalizing of the conclusion *)
-	    Proofview.V82.of_tactic (reduce
-	      (Genredexpr.Cbv
-		 { Redops.all_flags with
-		     Genredexpr.rDelta = false ;
-		     Genredexpr.rConst = []
-		 }
-	      )
-	      Locusops.onConcl);
-	    observe_tac ("toto ") tclIDTAC;
-    
+        tclTHENLIST
+          [
+            observe_tac("h_intro_patterns ")  (let l = (List.nth intro_pats (pred i)) in
+                                               match l with
+                                                 | [] -> tclIDTAC
+                                                 | _ -> Proofview.V82.of_tactic (intro_patterns false l));
+            (* unfolding of all the defined variables introduced by this branch *)
+            (* observe_tac "unfolding" pre_tac; *)
+            (* $zeta$ normalizing of the conclusion *)
+            Proofview.V82.of_tactic (reduce
+              (Genredexpr.Cbv
+                 { Redops.all_flags with
+                     Genredexpr.rDelta = false ;
+                     Genredexpr.rConst = []
+                 }
+              )
+              Locusops.onConcl);
+            observe_tac ("toto ") tclIDTAC;
+
             (* introducing the result of the graph and the equality hypothesis *)
-	    observe_tac "introducing" (tclMAP (fun x -> Proofview.V82.of_tactic (Simple.intro x)) [res;hres]);
-	    (* replacing [res] with its value *)
-	    observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres)));
-	    (* Conclusion *)
-	    observe_tac "exact" (fun g ->
-				 Proofview.V82.of_tactic (exact_check (app_constructor g)) g)  
-	  ]
+            observe_tac "introducing" (tclMAP (fun x -> Proofview.V82.of_tactic (Simple.intro x)) [res;hres]);
+            (* replacing [res] with its value *)
+            observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres)));
+            (* Conclusion *)
+            observe_tac "exact" (fun g ->
+                                 Proofview.V82.of_tactic (exact_check (app_constructor g)) g)
+          ]
       )
-	g
+        g
     in
     (* end of branche proof *)
     let lemmas =
@@ -379,44 +379,44 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
     *)
     let bindings =
       let params_bindings,avoid =
-	List.fold_left2
-	  (fun (bindings,avoid) decl p ->
-	     let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in
-	     p::bindings,id::avoid
-	  )
-	  ([],pf_ids_of_hyps g)
-	  princ_infos.params
-	  (List.rev params)
+        List.fold_left2
+          (fun (bindings,avoid) decl p ->
+             let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in
+             p::bindings,id::avoid
+          )
+          ([],pf_ids_of_hyps g)
+          princ_infos.params
+          (List.rev params)
       in
       let lemmas_bindings =
-	List.rev (fst  (List.fold_left2
-	  (fun (bindings,avoid) decl p ->
-	     let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in
+        List.rev (fst  (List.fold_left2
+          (fun (bindings,avoid) decl p ->
+             let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in
              (Reductionops.nf_zeta (pf_env g) (project g) p)::bindings,id::avoid)
-	  ([],avoid)
-	  princ_infos.predicates
-	  (lemmas)))
+          ([],avoid)
+          princ_infos.predicates
+          (lemmas)))
       in
       (params_bindings@lemmas_bindings)
     in
     tclTHENLIST
-      [ 
-	observe_tac "principle" (Proofview.V82.of_tactic (assert_by
-	  (Name principle_id)
-	  princ_type
-	  (exact_check f_principle)));
-	observe_tac "intro args_names" (tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) args_names);
-	(* observe_tac "titi" (pose_proof (Name (Id.of_string "__")) (Reductionops.nf_beta Evd.empty  ((mkApp (mkVar principle_id,Array.of_list bindings))))); *)
-	observe_tac "idtac" tclIDTAC;
-	tclTHEN_i
-	  (observe_tac
-	     "functional_induction" (
-	       (fun gl ->
-		let term = mkApp (mkVar principle_id,Array.of_list bindings) in
-		let gl', _ty = pf_eapply (Typing.type_of ~refresh:true)  gl term in
-		Proofview.V82.of_tactic (apply term) gl')
-	   ))
-	  (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g )
+      [
+        observe_tac "principle" (Proofview.V82.of_tactic (assert_by
+          (Name principle_id)
+          princ_type
+          (exact_check f_principle)));
+        observe_tac "intro args_names" (tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) args_names);
+        (* observe_tac "titi" (pose_proof (Name (Id.of_string "__")) (Reductionops.nf_beta Evd.empty  ((mkApp (mkVar principle_id,Array.of_list bindings))))); *)
+        observe_tac "idtac" tclIDTAC;
+        tclTHEN_i
+          (observe_tac
+             "functional_induction" (
+               (fun gl ->
+                let term = mkApp (mkVar principle_id,Array.of_list bindings) in
+                let gl', _ty = pf_eapply (Typing.type_of ~refresh:true)  gl term in
+                Proofview.V82.of_tactic (apply term) gl')
+           ))
+          (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g )
       ]
       g
 
@@ -431,7 +431,7 @@ let generalize_dependent_of x hyp g =
   tclMAP
     (function
        | LocalAssum ({binder_name=id},t) when not (Id.equal id hyp) &&
-	   (Termops.occur_var (pf_env g) (project g) x t) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id])
+           (Termops.occur_var (pf_env g) (project g) x t) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id])
        | _ -> tclIDTAC
     )
     (pf_hyps g)
@@ -458,99 +458,99 @@ and intros_with_rewrite_aux : Tacmach.tactic =
     let sigma = project g in
     match EConstr.kind sigma (pf_concl g) with
           | Prod(_,t,t') ->
-	      begin
-		match EConstr.kind sigma t with
-		  | App(eq,args) when (EConstr.eq_constr sigma eq eq_ind)  ->
- 		      if Reductionops.is_conv (pf_env g) (project g) args.(1) args.(2)
-		      then
-			let id = pf_get_new_id (Id.of_string "y") g  in
-			tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id); thin [id]; intros_with_rewrite ] g
-		      else if isVar sigma args.(1) && (Environ.evaluable_named (destVar sigma args.(1)) (pf_env g)) 
-		      then tclTHENLIST[
-			Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(1)))]);
-			tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(1)))] ((destVar sigma args.(1)),Locus.InHyp) )))
-			  (pf_ids_of_hyps g);
-			intros_with_rewrite
-		      ] g
-		      else if isVar sigma args.(2) && (Environ.evaluable_named (destVar sigma args.(2)) (pf_env g)) 
-		      then tclTHENLIST[
-			Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(2)))]);
-			tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(2)))] ((destVar sigma args.(2)),Locus.InHyp) )))
-			  (pf_ids_of_hyps g);
-			intros_with_rewrite
-		      ] g
-		      else if isVar sigma args.(1)
-		      then
-			let id = pf_get_new_id (Id.of_string "y") g  in
-			tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id);
-				     generalize_dependent_of (destVar sigma args.(1)) id;
-				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id)));
-				     intros_with_rewrite
-				   ]
-			  g
-		      else if isVar sigma args.(2) 
-		      then 
-			let id = pf_get_new_id (Id.of_string "y") g  in
-			tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id);
-				     generalize_dependent_of (destVar sigma args.(2)) id;
-				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar id)));
-				     intros_with_rewrite
-				   ]
-			  g
-		      else
-			begin
-			  let id = pf_get_new_id (Id.of_string "y") g  in
-			  tclTHENLIST[
-			    Proofview.V82.of_tactic (Simple.intro id);
-			    tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id)));
-			    intros_with_rewrite
-			  ] g
-			end
+              begin
+                match EConstr.kind sigma t with
+                  | App(eq,args) when (EConstr.eq_constr sigma eq eq_ind)  ->
+                      if Reductionops.is_conv (pf_env g) (project g) args.(1) args.(2)
+                      then
+                        let id = pf_get_new_id (Id.of_string "y") g  in
+                        tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id); thin [id]; intros_with_rewrite ] g
+                      else if isVar sigma args.(1) && (Environ.evaluable_named (destVar sigma args.(1)) (pf_env g))
+                      then tclTHENLIST[
+                        Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(1)))]);
+                        tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(1)))] ((destVar sigma args.(1)),Locus.InHyp) )))
+                          (pf_ids_of_hyps g);
+                        intros_with_rewrite
+                      ] g
+                      else if isVar sigma args.(2) && (Environ.evaluable_named (destVar sigma args.(2)) (pf_env g))
+                      then tclTHENLIST[
+                        Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(2)))]);
+                        tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(2)))] ((destVar sigma args.(2)),Locus.InHyp) )))
+                          (pf_ids_of_hyps g);
+                        intros_with_rewrite
+                      ] g
+                      else if isVar sigma args.(1)
+                      then
+                        let id = pf_get_new_id (Id.of_string "y") g  in
+                        tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id);
+                                     generalize_dependent_of (destVar sigma args.(1)) id;
+                                     tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id)));
+                                     intros_with_rewrite
+                                   ]
+                          g
+                      else if isVar sigma args.(2)
+                      then
+                        let id = pf_get_new_id (Id.of_string "y") g  in
+                        tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id);
+                                     generalize_dependent_of (destVar sigma args.(2)) id;
+                                     tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar id)));
+                                     intros_with_rewrite
+                                   ]
+                          g
+                      else
+                        begin
+                          let id = pf_get_new_id (Id.of_string "y") g  in
+                          tclTHENLIST[
+                            Proofview.V82.of_tactic (Simple.intro id);
+                            tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id)));
+                            intros_with_rewrite
+                          ] g
+                        end
                   | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type")) ->
-		      Proofview.V82.of_tactic tauto g
-		  | Case(_,_,v,_) ->
-		      tclTHENLIST[
-			Proofview.V82.of_tactic (simplest_case v);
-			intros_with_rewrite
-		      ] g
-		  | LetIn _ ->
-		      tclTHENLIST[
-			Proofview.V82.of_tactic (reduce
-			  (Genredexpr.Cbv
-			     {Redops.all_flags
-			      with Genredexpr.rDelta = false;
-			     })
-			  Locusops.onConcl)
-			;
-			intros_with_rewrite
-		      ] g
-		  | _ ->
-		      let id = pf_get_new_id (Id.of_string "y") g  in
-		      tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id);intros_with_rewrite] g
-	      end
-	  | LetIn _ ->
-	      tclTHENLIST[
-		Proofview.V82.of_tactic (reduce
-		  (Genredexpr.Cbv
-		     {Redops.all_flags
-		      with Genredexpr.rDelta = false;
-		     })
-		  Locusops.onConcl)
-		;
-		intros_with_rewrite
-	      ] g
-	  | _ -> tclIDTAC g
+                      Proofview.V82.of_tactic tauto g
+                  | Case(_,_,v,_) ->
+                      tclTHENLIST[
+                        Proofview.V82.of_tactic (simplest_case v);
+                        intros_with_rewrite
+                      ] g
+                  | LetIn _ ->
+                      tclTHENLIST[
+                        Proofview.V82.of_tactic (reduce
+                          (Genredexpr.Cbv
+                             {Redops.all_flags
+                              with Genredexpr.rDelta = false;
+                             })
+                          Locusops.onConcl)
+                        ;
+                        intros_with_rewrite
+                      ] g
+                  | _ ->
+                      let id = pf_get_new_id (Id.of_string "y") g  in
+                      tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id);intros_with_rewrite] g
+              end
+          | LetIn _ ->
+              tclTHENLIST[
+                Proofview.V82.of_tactic (reduce
+                  (Genredexpr.Cbv
+                     {Redops.all_flags
+                      with Genredexpr.rDelta = false;
+                     })
+                  Locusops.onConcl)
+                ;
+                intros_with_rewrite
+              ] g
+          | _ -> tclIDTAC g
 
 let rec reflexivity_with_destruct_cases g =
   let destruct_case () =
     try
       match EConstr.kind (project g) (snd (destApp (project g) (pf_concl g))).(2) with
-	| Case(_,_,v,_) ->
-	    tclTHENLIST[
-	      Proofview.V82.of_tactic (simplest_case v);
-	      Proofview.V82.of_tactic intros;
-	      observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
-	    ]
+        | Case(_,_,v,_) ->
+            tclTHENLIST[
+              Proofview.V82.of_tactic (simplest_case v);
+              Proofview.V82.of_tactic intros;
+              observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
+            ]
         | _ -> Proofview.V82.of_tactic reflexivity
     with e when CErrors.noncritical e -> Proofview.V82.of_tactic reflexivity
   in
@@ -563,27 +563,27 @@ let rec reflexivity_with_destruct_cases g =
   let discr_inject =
     Tacticals.onAllHypsAndConcl (
        fun sc g ->
-	 match sc with
-	     None -> tclIDTAC g
-	   | Some id ->
-	       match EConstr.kind (project g) (pf_unsafe_type_of g (mkVar id)) with
-		 | App(eq,[|_;t1;t2|]) when EConstr.eq_constr (project g) eq eq_ind ->
-		     if Equality.discriminable (pf_env g) (project g) t1 t2
-		     then Proofview.V82.of_tactic (Equality.discrHyp id) g
-		     else if Equality.injectable (pf_env g) (project g) ~keep_proofs:None t1 t2
-		     then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp my_inj_flags None id);thin [id];intros_with_rewrite]  g
-		     else tclIDTAC g
-		 | _ -> tclIDTAC g
+         match sc with
+             None -> tclIDTAC g
+           | Some id ->
+               match EConstr.kind (project g) (pf_unsafe_type_of g (mkVar id)) with
+                 | App(eq,[|_;t1;t2|]) when EConstr.eq_constr (project g) eq eq_ind ->
+                     if Equality.discriminable (pf_env g) (project g) t1 t2
+                     then Proofview.V82.of_tactic (Equality.discrHyp id) g
+                     else if Equality.injectable (pf_env g) (project g) ~keep_proofs:None t1 t2
+                     then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp my_inj_flags None id);thin [id];intros_with_rewrite]  g
+                     else tclIDTAC g
+                 | _ -> tclIDTAC g
     )
   in
   (tclFIRST
     [ observe_tac "reflexivity_with_destruct_cases : reflexivity" (Proofview.V82.of_tactic reflexivity);
       observe_tac "reflexivity_with_destruct_cases : destruct_case" ((destruct_case ()));
       (*  We reach this point ONLY if
-	  the same value is matched (at least) two times
-	  along binding path.
-	  In this case, either we have a discriminable hypothesis and we are done,
-	  either at least an injectable one and we do the injection before continuing
+          the same value is matched (at least) two times
+          along binding path.
+          In this case, either we have a discriminable hypothesis and we are done,
+          either at least an injectable one and we do the injection before continuing
       *)
       observe_tac "reflexivity_with_destruct_cases : others" (tclTHEN (tclPROGRESS discr_inject ) reflexivity_with_destruct_cases)
     ])
@@ -626,7 +626,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti
     let lemmas =
       Array.map
         (fun (_,(ctxt,concl)) -> Reductionops.nf_zeta (pf_env g) (project g) (EConstr.it_mkLambda_or_LetIn concl ctxt))
-	lemmas_types_infos
+        lemmas_types_infos
     in
     (* We get the constant and the principle corresponding to this lemma *)
     let f = funcs.(i) in
@@ -642,8 +642,8 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti
     (* and fresh names for res H and the principle (cf bug bug #1174) *)
     let res,hres,graph_principle_id =
       match generate_fresh_id (Id.of_string "z") ids 3 with
-	| [res;hres;graph_principle_id] -> res,hres,graph_principle_id
-	| _ -> assert false
+        | [res;hres;graph_principle_id] -> res,hres,graph_principle_id
+        | _ -> assert false
     in
     let ids = res::hres::graph_principle_id::ids in
     (* we also compute fresh names for each hyptohesis of each branch
@@ -651,12 +651,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti
     let branches = List.rev princ_infos.branches in
     let intro_pats =
       List.map
-	(fun decl ->
-	   List.map
-	     (fun id -> id)
-	     (generate_fresh_id (Id.of_string "y") ids (nb_prod (project g) (RelDecl.get_type decl)))
-	)
-	branches
+        (fun decl ->
+           List.map
+             (fun id -> id)
+             (generate_fresh_id (Id.of_string "y") ids (nb_prod (project g) (RelDecl.get_type decl)))
+        )
+        branches
     in
     (* We will need to change the function by its body
        using [f_equation] if it is recursive (that is the graph is infinite
@@ -671,25 +671,25 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti
       if infos.is_general
         || Rtree.is_infinite Declareops.eq_recarg graph_def.mind_recargs
       then
-	let eq_lemma =
-	  try Option.get (infos).equation_lemma
-	  with Option.IsNone -> anomaly (Pp.str "Cannot find equation lemma.")
-	in
-	tclTHENLIST[
-	  tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) ids;
-	  Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma));
-	  (* Don't forget to $\zeta$ normlize the term since the principles
+        let eq_lemma =
+          try Option.get (infos).equation_lemma
+          with Option.IsNone -> anomaly (Pp.str "Cannot find equation lemma.")
+        in
+        tclTHENLIST[
+          tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) ids;
+          Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma));
+          (* Don't forget to $\zeta$ normlize the term since the principles
              have been $\zeta$-normalized *)
-	  Proofview.V82.of_tactic (reduce
-	    (Genredexpr.Cbv
-	       {Redops.all_flags
-		with Genredexpr.rDelta = false;
-	       })
-	    Locusops.onConcl)
-	  ;
-	  Proofview.V82.of_tactic (generalize (List.map mkVar ids));
-	  thin ids
-	]
+          Proofview.V82.of_tactic (reduce
+            (Genredexpr.Cbv
+               {Redops.all_flags
+                with Genredexpr.rDelta = false;
+               })
+            Locusops.onConcl)
+          ;
+          Proofview.V82.of_tactic (generalize (List.map mkVar ids));
+          thin ids
+        ]
       else
         Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst (destConst (project g) f)))])
     in
@@ -699,39 +699,39 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti
     let prove_branche i g =
       (* we fist compute the inductive corresponding to the branch *)
       let this_ind_number =
-	let constructor_num = i - !min_constr_number in
-	let length = Array.length (graphs.(!ind_number).Declarations.mind_consnames) in
-	if constructor_num <= length
-	then !ind_number
-	else
-	  begin
-	    incr ind_number;
-	    min_constr_number := !min_constr_number + length;
-	    !ind_number
-	  end
+        let constructor_num = i - !min_constr_number in
+        let length = Array.length (graphs.(!ind_number).Declarations.mind_consnames) in
+        if constructor_num <= length
+        then !ind_number
+        else
+          begin
+            incr ind_number;
+            min_constr_number := !min_constr_number + length;
+            !ind_number
+          end
       in
       let this_branche_ids = List.nth intro_pats (pred i) in
       tclTHENLIST[
-	(* we expand the definition of the function *)
+        (* we expand the definition of the function *)
         observe_tac "rewrite_tac" (rewrite_tac this_ind_number this_branche_ids);
-	(* introduce hypothesis with some rewrite *)
+        (* introduce hypothesis with some rewrite *)
         observe_tac "intros_with_rewrite (all)" intros_with_rewrite;
-	(* The proof is (almost) complete *)
+        (* The proof is (almost) complete *)
         observe_tac "reflexivity" (reflexivity_with_destruct_cases)
       ]
-	g
+        g
     in
     let params_names = fst (List.chop princ_infos.nparams args_names) in
     let open EConstr in
     let params = List.map mkVar params_names in
     tclTHENLIST
       [ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) (args_names@[res;hres]);
-	observe_tac "h_generalize"
-	(Proofview.V82.of_tactic (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]));
-	Proofview.V82.of_tactic (Simple.intro graph_principle_id);
-	observe_tac "" (tclTHEN_i
-	  (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings)))))
-	  (fun i g -> observe_tac "prove_branche" (prove_branche i) g ))
+        observe_tac "h_generalize"
+        (Proofview.V82.of_tactic (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]));
+        Proofview.V82.of_tactic (Simple.intro graph_principle_id);
+        observe_tac "" (tclTHEN_i
+          (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings)))))
+          (fun i g -> observe_tac "prove_branche" (prove_branche i) g ))
       ]
       g
 
@@ -752,105 +752,105 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
   funind_purify
     (fun () ->
      let env = Global.env () in
-     let evd = ref (Evd.from_env env) in 
+     let evd = ref (Evd.from_env env) in
      let graphs_constr = Array.map mkInd graphs in
      let lemmas_types_infos =
        Util.Array.map2_i
-	 (fun i f_constr graph ->
-	 (* let const_of_f,u = destConst f_constr in *)
-	 let (type_of_lemma_ctxt,type_of_lemma_concl,graph) =
-	   generate_type evd false f_constr graph i
-	 in
-	 let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
-	 graphs_constr.(i) <- graph;
-	 let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
+         (fun i f_constr graph ->
+         (* let const_of_f,u = destConst f_constr in *)
+         let (type_of_lemma_ctxt,type_of_lemma_concl,graph) =
+           generate_type evd false f_constr graph i
+         in
+         let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
+         graphs_constr.(i) <- graph;
+         let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
          let sigma, _ = Typing.type_of (Global.env ()) !evd type_of_lemma in
          evd := sigma;
            let type_of_lemma = Reductionops.nf_zeta (Global.env ()) !evd type_of_lemma in
-	   observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env (Global.env ()) !evd type_of_lemma);
-	   type_of_lemma,type_info
-	)
-	funs_constr
-	graphs_constr
+           observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env (Global.env ()) !evd type_of_lemma);
+           type_of_lemma,type_info
+        )
+        funs_constr
+        graphs_constr
     in
     let schemes =
       (* The functional induction schemes are computed and not saved if there is more that one function
-	 if the block contains only one function we can safely reuse [f_rect]
+         if the block contains only one function we can safely reuse [f_rect]
        *)
       try
-	if not (Int.equal (Array.length funs_constr) 1) then raise Not_found;
-	[| find_induction_principle evd funs_constr.(0) |]
+        if not (Int.equal (Array.length funs_constr) 1) then raise Not_found;
+        [| find_induction_principle evd funs_constr.(0) |]
       with Not_found ->
-	(
-	
-	  Array.of_list
-	    (List.map
-	       (fun entry ->
-		  (EConstr.of_constr (fst (fst(Future.force entry.Entries.const_entry_body))), EConstr.of_constr (Option.get entry.Entries.const_entry_type ))
-	       )
-	       (make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs))
-	    )
-	)
+        (
+
+          Array.of_list
+            (List.map
+               (fun entry ->
+                  (EConstr.of_constr (fst (fst(Future.force entry.Entries.const_entry_body))), EConstr.of_constr (Option.get entry.Entries.const_entry_type ))
+               )
+               (make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs))
+            )
+        )
     in
     let proving_tac =
       prove_fun_correct !evd funs_constr graphs_constr schemes lemmas_types_infos
     in
     Array.iteri
       (fun i f_as_constant ->
-	 let f_id = Label.to_id (Constant.label (fst f_as_constant)) in
-	 (*i The next call to mk_correct_id is valid since we are constructing the lemma
-	     Ensures by: obvious
-	 i*)
-	 let lem_id = mk_correct_id f_id in
+         let f_id = Label.to_id (Constant.label (fst f_as_constant)) in
+         (*i The next call to mk_correct_id is valid since we are constructing the lemma
+             Ensures by: obvious
+         i*)
+         let lem_id = mk_correct_id f_id in
          let (typ,_) = lemmas_types_infos.(i) in
          let lemma = Lemmas.start_lemma
-	   lem_id
+           lem_id
            Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
            !evd
            typ in
          let lemma = fst @@ Lemmas.by
-		   (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
+                   (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
                                                       (proving_tac i))) lemma in
          let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in
-	 let finfo = find_Function_infos (fst f_as_constant) in
-	 (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *)
-	 let _,lem_cst_constr = Evd.fresh_global
-				  (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
+         let finfo = find_Function_infos (fst f_as_constant) in
+         (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *)
+         let _,lem_cst_constr = Evd.fresh_global
+                                  (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
          let (lem_cst,_) = destConst !evd lem_cst_constr in
-	 update_Function {finfo with correctness_lemma = Some lem_cst};
+         update_Function {finfo with correctness_lemma = Some lem_cst};
 
       )
       funs;
     let lemmas_types_infos =
       Util.Array.map2_i
-	(fun i f_constr graph ->
-	 let (type_of_lemma_ctxt,type_of_lemma_concl,graph)   =
-	   generate_type evd true f_constr graph i
-	 in
-	 let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
-	 graphs_constr.(i) <- graph;
-	 let type_of_lemma =
-	   EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt
-	 in
+        (fun i f_constr graph ->
+         let (type_of_lemma_ctxt,type_of_lemma_concl,graph)   =
+           generate_type evd true f_constr graph i
+         in
+         let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
+         graphs_constr.(i) <- graph;
+         let type_of_lemma =
+           EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt
+         in
          let type_of_lemma = Reductionops.nf_zeta env !evd type_of_lemma in
          observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env env !evd type_of_lemma);
-	 type_of_lemma,type_info
-	)
-	funs_constr
-	graphs_constr
+         type_of_lemma,type_info
+        )
+        funs_constr
+        graphs_constr
     in
 
     let (kn,_) as graph_ind,u  = (destInd !evd graphs_constr.(0)) in
     let mib,mip = Global.lookup_inductive graph_ind in
-    let sigma, scheme = 
-	(Indrec.build_mutual_induction_scheme (Global.env ()) !evd
-	   (Array.to_list
-	      (Array.mapi
-		 (fun i _ -> ((kn,i), EInstance.kind !evd u),true,InType)
-		 mib.Declarations.mind_packets
-	      )
-	   )
-	)
+    let sigma, scheme =
+        (Indrec.build_mutual_induction_scheme (Global.env ()) !evd
+           (Array.to_list
+              (Array.mapi
+                 (fun i _ -> ((kn,i), EInstance.kind !evd u),true,InType)
+                 mib.Declarations.mind_packets
+              )
+           )
+        )
     in
     let schemes =
       Array.of_list scheme
@@ -860,23 +860,23 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
     in
     Array.iteri
       (fun i f_as_constant ->
-	 let f_id = Label.to_id (Constant.label (fst f_as_constant)) in
-	 (*i The next call to mk_complete_id is valid since we are constructing the lemma
-	     Ensures by: obvious
-	   i*)
-	 let lem_id = mk_complete_id f_id in
+         let f_id = Label.to_id (Constant.label (fst f_as_constant)) in
+         (*i The next call to mk_complete_id is valid since we are constructing the lemma
+             Ensures by: obvious
+           i*)
+         let lem_id = mk_complete_id f_id in
          let lemma = Lemmas.start_lemma lem_id
            Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) sigma
          (fst lemmas_types_infos.(i)) in
          let lemma = fst (Lemmas.by
-	   (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
+           (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
               (proving_tac i))) lemma) in
          let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in
-	 let finfo = find_Function_infos (fst f_as_constant) in
-	 let _,lem_cst_constr = Evd.fresh_global
-				  (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
+         let finfo = find_Function_infos (fst f_as_constant) in
+         let _,lem_cst_constr = Evd.fresh_global
+                                  (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
          let (lem_cst,_) = destConst !evd lem_cst_constr in
-	 update_Function {finfo with completeness_lemma = Some lem_cst}
+         update_Function {finfo with completeness_lemma = Some lem_cst}
       )
       funs)
     ()
@@ -894,31 +894,31 @@ let revert_graph kn post_tac hid g =
     let typ = pf_unsafe_type_of g (mkVar hid) in
     match EConstr.kind sigma typ with
       | App(i,args) when isInd sigma i ->
-	  let ((kn',num) as ind'),u = destInd sigma i in
-	  if MutInd.equal kn kn'
-	  then (* We have generated a graph hypothesis so that we must change it if we can *)
-	    let info =
-	      try find_Function_of_graph ind'
-	      with Not_found -> (* The graphs are mutually recursive but we cannot find one of them !*)
-		anomaly (Pp.str "Cannot retrieve infos about a mutual block.")
-	    in
-	    (* if we can find a completeness lemma for this function
-	       then we can come back to the functional form. If not, we do nothing
-	    *)
-	    match info.completeness_lemma with
-	      | None -> tclIDTAC g
-	      | Some f_complete ->
-		  let f_args,res = Array.chop (Array.length args - 1) args in
-		  tclTHENLIST
-		    [
-		      Proofview.V82.of_tactic (generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]);
-		      thin [hid];
-		      Proofview.V82.of_tactic (Simple.intro hid);
-		      post_tac hid
-		    ]
-		    g
-
-	  else tclIDTAC g
+          let ((kn',num) as ind'),u = destInd sigma i in
+          if MutInd.equal kn kn'
+          then (* We have generated a graph hypothesis so that we must change it if we can *)
+            let info =
+              try find_Function_of_graph ind'
+              with Not_found -> (* The graphs are mutually recursive but we cannot find one of them !*)
+                anomaly (Pp.str "Cannot retrieve infos about a mutual block.")
+            in
+            (* if we can find a completeness lemma for this function
+               then we can come back to the functional form. If not, we do nothing
+            *)
+            match info.completeness_lemma with
+              | None -> tclIDTAC g
+              | Some f_complete ->
+                  let f_args,res = Array.chop (Array.length args - 1) args in
+                  tclTHENLIST
+                    [
+                      Proofview.V82.of_tactic (generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]);
+                      thin [hid];
+                      Proofview.V82.of_tactic (Simple.intro hid);
+                      post_tac hid
+                    ]
+                    g
+
+          else tclIDTAC g
       | _ -> tclIDTAC g
 
 
@@ -946,25 +946,25 @@ let functional_inversion kn hid fconst f_correct : Tacmach.tactic =
     let type_of_h = pf_unsafe_type_of g (mkVar hid) in
     match EConstr.kind sigma type_of_h with
       | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ())  ->
-	  let pre_tac,f_args,res =
-	    match EConstr.kind sigma args.(1),EConstr.kind sigma args.(2) with
-	      | App(f,f_args),_ when EConstr.eq_constr sigma f fconst ->
-		  ((fun hid -> Proofview.V82.of_tactic (intros_symmetry (Locusops.onHyp hid))),f_args,args.(2))
-	      |_,App(f,f_args) when EConstr.eq_constr sigma f fconst ->
-		 ((fun hid -> tclIDTAC),f_args,args.(1))
-	      | _ -> (fun hid -> tclFAIL 1 (mt ())),[||],args.(2)
-	  in
-	  tclTHENLIST [
-	    pre_tac hid;
-	    Proofview.V82.of_tactic (generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]);
-	    thin [hid];
-	    Proofview.V82.of_tactic (Simple.intro hid);
+          let pre_tac,f_args,res =
+            match EConstr.kind sigma args.(1),EConstr.kind sigma args.(2) with
+              | App(f,f_args),_ when EConstr.eq_constr sigma f fconst ->
+                  ((fun hid -> Proofview.V82.of_tactic (intros_symmetry (Locusops.onHyp hid))),f_args,args.(2))
+              |_,App(f,f_args) when EConstr.eq_constr sigma f fconst ->
+                 ((fun hid -> tclIDTAC),f_args,args.(1))
+              | _ -> (fun hid -> tclFAIL 1 (mt ())),[||],args.(2)
+          in
+          tclTHENLIST [
+            pre_tac hid;
+            Proofview.V82.of_tactic (generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]);
+            thin [hid];
+            Proofview.V82.of_tactic (Simple.intro hid);
             Proofview.V82.of_tactic (Inv.inv Inv.FullInversion None (NamedHyp hid));
-	    (fun g ->
-	       let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps g) in
-	       tclMAP (revert_graph kn pre_tac)  (hid::new_ids)  g
-	    );
-	  ] g
+            (fun g ->
+               let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps g) in
+               tclMAP (revert_graph kn pre_tac)  (hid::new_ids)  g
+            );
+          ] g
       | _ -> tclFAIL 1 (mt ()) g
 
 
@@ -994,46 +994,46 @@ let invfun qhyp f g =
     | Some f -> invfun qhyp f g
     | None ->
        Proofview.V82.of_tactic begin
-	Tactics.try_intros_until
-	  (fun hid -> Proofview.V82.tactic begin fun g ->
+        Tactics.try_intros_until
+          (fun hid -> Proofview.V82.tactic begin fun g ->
             let sigma = project g in
-	     let hyp_typ = pf_unsafe_type_of g (mkVar hid)  in
-	     match EConstr.kind sigma hyp_typ with
-	       | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) ->
-		   begin
-		     let f1,_ = decompose_app sigma args.(1) in
-		     try
-		       if not (isConst sigma f1) then raise NoFunction;
-		       let finfos = find_Function_infos (fst (destConst sigma f1)) in
-		       let f_correct = mkConst(Option.get finfos.correctness_lemma)
-		       and kn = fst finfos.graph_ind
-		       in
-		       functional_inversion kn hid f1 f_correct g
-		     with | NoFunction | Option.IsNone | Not_found ->
-		       try
-			 let f2,_ = decompose_app sigma args.(2) in
-			 if not (isConst sigma f2) then raise NoFunction;
-			 let finfos = find_Function_infos (fst (destConst sigma f2)) in
-			 let f_correct = mkConst(Option.get finfos.correctness_lemma)
-			 and kn = fst finfos.graph_ind
-			 in
-			 functional_inversion kn hid  f2 f_correct g
-		       with
-			 | NoFunction ->
-			     user_err  (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function")
-			 | Option.IsNone  ->
-			     if do_observe ()
-			     then
-			       error "Cannot use equivalence with graph for any side of the equality"
-			     else user_err  (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
-			 | Not_found ->
-			     if do_observe ()
-			     then
-			       error "No graph found for any side of equality"
-			     else user_err  (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
-		   end
-	       | _ -> user_err  (Ppconstr.pr_id hid ++ str " must be an equality ")
-	  end)
-	  qhyp
+             let hyp_typ = pf_unsafe_type_of g (mkVar hid)  in
+             match EConstr.kind sigma hyp_typ with
+               | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) ->
+                   begin
+                     let f1,_ = decompose_app sigma args.(1) in
+                     try
+                       if not (isConst sigma f1) then raise NoFunction;
+                       let finfos = find_Function_infos (fst (destConst sigma f1)) in
+                       let f_correct = mkConst(Option.get finfos.correctness_lemma)
+                       and kn = fst finfos.graph_ind
+                       in
+                       functional_inversion kn hid f1 f_correct g
+                     with | NoFunction | Option.IsNone | Not_found ->
+                       try
+                         let f2,_ = decompose_app sigma args.(2) in
+                         if not (isConst sigma f2) then raise NoFunction;
+                         let finfos = find_Function_infos (fst (destConst sigma f2)) in
+                         let f_correct = mkConst(Option.get finfos.correctness_lemma)
+                         and kn = fst finfos.graph_ind
+                         in
+                         functional_inversion kn hid  f2 f_correct g
+                       with
+                         | NoFunction ->
+                             user_err  (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function")
+                         | Option.IsNone  ->
+                             if do_observe ()
+                             then
+                               error "Cannot use equivalence with graph for any side of the equality"
+                             else user_err  (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+                         | Not_found ->
+                             if do_observe ()
+                             then
+                               error "No graph found for any side of equality"
+                             else user_err  (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+                   end
+               | _ -> user_err  (Ppconstr.pr_id hid ++ str " must be an equality ")
+          end)
+          qhyp
           end
-	  g
+          g