petit nettoyage de kernel/inductive

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2460 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 10 insertions, 11 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index c6057367e8..5e920ea5ac 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -172,7 +172,7 @@ and mk_casegoals sigma goal goalacc p c =
   let pj = {uj_val=p; uj_type=pt} in 
   let indspec =
     try find_mrectype env sigma ct
-    with Induc -> anomaly "mk_casegoals" in
+    with Not_found -> anomaly "mk_casegoals" in
   let (lbrty,conclty) =
     type_case_branches_with_names env indspec pj c in
   (acc'',lbrty,conclty)
@@ -463,7 +463,7 @@ let prim_refiner r sigma goal =
             	if k = 1 then 
 		  try 
 		    let _ = find_inductive env sigma c1 in ()
-		  with Induc -> 
+		  with Not_found -> 
 		    error "cannot do a fixpoint on a non inductive type"
             	else 
 		  check_ind (k-1) b
@@ -482,7 +482,7 @@ let prim_refiner r sigma goal =
             	if k = 1 then 
 		  try 
 		    fst (find_inductive env sigma c1)
-		  with Induc -> 
+		  with Not_found -> 
 		    error "cannot do a fixpoint on a non inductive type"
             	else 
 		  check_ind (k-1) b
@@ -513,7 +513,7 @@ let prim_refiner r sigma goal =
             | _ -> 
 		try 
 		  let _ = find_coinductive env sigma b in ()
-                with Induc -> 
+                with Not_found -> 
 		  error ("All methods must construct elements " ^
 			  "in coinductive types")
 	in
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 8e2a9b0eaf..7c51526726 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -85,11 +85,11 @@ let get_hyps  evc = evc.it
 let get_env   evc = Global.env_of_context evc.it
 let get_gc    evc = evc.sigma
 
-let pf_lookup_name_as_renamed hyps ccl s =
-  Detyping.lookup_name_as_renamed hyps ccl s
+let pf_lookup_name_as_renamed env ccl s =
+  Detyping.lookup_name_as_renamed env ccl s
 
-let pf_lookup_index_as_renamed ccl n =
-  Detyping.lookup_index_as_renamed ccl n
+let pf_lookup_index_as_renamed env ccl n =
+  Detyping.lookup_index_as_renamed env ccl n
 
 (*********************************************************************)
 (*                  Pretty printing functions                        *)
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index 200adac0ac..d6a1a51d5f 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -42,9 +42,8 @@ val get_hyps  : named_context sigma -> named_context
 val get_env   : named_context sigma -> env
 val get_gc    : named_context sigma -> evar_map
 
-val pf_lookup_name_as_renamed : 
-  named_context -> constr -> identifier -> int option
-val pf_lookup_index_as_renamed : constr -> int -> int option
+val pf_lookup_name_as_renamed  : env -> constr -> identifier -> int option
+val pf_lookup_index_as_renamed : env -> constr -> int -> int option
 
 
 (*s Pretty printing functions. *)