3 files changed, 6 insertions, 6 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index c55040df03..4c59996aa7 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -55,7 +55,8 @@ let ind_hyps env sigma nevar ind largs =
   let types= Inductiveops.arities_of_constructors env ind in
   let myhyps t =
     let t = EConstr.of_constr t in
-    let t1=Termops.prod_applist sigma t largs in
+    let nparam_decls = Context.Rel.length (fst (Global.lookup_inductive (fst ind))).mind_params_ctxt in
+    let t1=Termops.prod_applist_assum sigma nparam_decls t largs in
     let t2=snd (decompose_prod_n_assum sigma nevar t1) in
       fst (decompose_prod_assum sigma t2) in
     Array.map myhyps types
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 938bec25b9..3c6ab47e9b 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma"  i*)
 
 open Ltac_plugin
 open Formula
@@ -40,17 +39,17 @@ let _=
   in
     declare_int_option gdopt
 
-let congruence_depth=ref 100
 
 let _=
+  let congruence_depth=ref 100 in
   let gdopt=
-    { optdepr=false;
+    { optdepr=true; (* noop *)
       optname="Congruence Depth";
       optkey=["Congruence";"Depth"];
       optread=(fun ()->Some !congruence_depth);
       optwrite=
    (function
-	None->congruence_depth:=0
+        None->congruence_depth:=0
       |	Some i->congruence_depth:=(max i 0))}
   in
     declare_int_option gdopt
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index d462013353..09147d606c 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -37,7 +37,7 @@ let ground_tac solver startseq =
     let () =
       if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
       then
-        let gl = { Evd.it = Proofview.Goal.goal (Proofview.Goal.assume gl); sigma = project gl } in
+        let gl = { Evd.it = Proofview.Goal.goal gl; sigma = project gl } in
         Feedback.msg_debug (Printer.pr_goal gl)
     in
     tclORELSE (axiom_tac seq.gl seq)