Move is_prim... to Inductiveops and correct Scheme

Now scheme will not try to build ill-typed dependent analyses
on recursive records with primitive projections but report
a proper error.

Minor change of the API (adding one error case to recursion_scheme_error).

1 files changed, 5 insertions, 2 deletions

diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index f0736d2dd..192b64a5e 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -16,6 +16,7 @@ open Evd
 type recursion_scheme_error =
   | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * pinductive
   | NotMutualInScheme of inductive * inductive
+  | NotAllowedDependentAnalysis of (*isrec:*) bool * inductive
 
 exception RecursionSchemeError of recursion_scheme_error
 
@@ -28,13 +29,15 @@ type dep_flag = bool
 val build_case_analysis_scheme : env -> 'r Sigma.t -> pinductive ->
       dep_flag -> sorts_family -> (constr, 'r) Sigma.sigma
 
-(** Build a dependent case elimination predicate unless type is in Prop *)
+(** Build a dependent case elimination predicate unless type is in Prop
+   or is a recursive record with primitive projections. *)
 
 val build_case_analysis_scheme_default : env -> 'r Sigma.t -> pinductive ->
       sorts_family -> (constr, 'r) Sigma.sigma
 
 (** Builds a recursive induction scheme (Peano-induction style) in the same
-   sort family as the inductive family; it is dependent if not in Prop *)
+   sort family as the inductive family; it is dependent if not in Prop
+   or a recursive record with primitive projections.  *)
 
 val build_induction_scheme : env -> evar_map -> pinductive ->
       dep_flag -> sorts_family -> evar_map * constr