diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 12 | ||||
| -rw-r--r-- | library/declare.mli | 7 | ||||
| -rw-r--r-- | library/indrec.ml | 20 | ||||
| -rw-r--r-- | library/indrec.mli | 9 |
4 files changed, 27 insertions, 21 deletions
diff --git a/library/declare.ml b/library/declare.ml index 6809b6e554..c07a8577f7 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -523,12 +523,13 @@ let instantiate_inductive_section_params t ind = else t (* Eliminations. *) -let eliminations = [ (prop,"_ind") ; (spec,"_rec") ; (types,"_rect") ] +let eliminations = + [ (ElimOnProp,"_ind") ; (ElimOnSet,"_rec") ; (ElimOnType,"_rect") ] let elimination_suffix = function - | Type _ -> "_rect" - | Prop Null -> "_ind" - | Prop Pos -> "_rec" + | ElimOnProp -> "_ind" + | ElimOnSet -> "_rec" + | ElimOnType -> "_rect" let make_elimination_ident id s = add_suffix id (elimination_suffix s) @@ -551,7 +552,8 @@ let declare_one_elimination mispec = let kelim = mis_kelim mispec in List.iter (fun (sort,suff) -> - if List.mem sort kelim then declare (mindstr^suff) (make_elim sort)) + if List.mem sort kelim then + declare (mindstr^suff) (make_elim (sort_of_elimination sort))) eliminations let declare_eliminations sp = diff --git a/library/declare.mli b/library/declare.mli index c623a0cce2..e17be37e3a 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -117,6 +117,7 @@ val path_of_inductive_path : inductive_path -> mutual_inductive_path val path_of_constructor_path : constructor_path -> mutual_inductive_path (* Look up function for the default elimination constant *) -val elimination_suffix : sorts -> string -val make_elimination_ident : inductive_ident:identifier -> sorts -> identifier -val lookup_eliminator : Environ.env -> inductive -> sorts -> constr +val elimination_suffix : elimination_sorts -> string +val make_elimination_ident : + inductive_ident:identifier -> elimination_sorts -> identifier +val lookup_eliminator : Environ.env -> inductive -> elimination_sorts -> constr diff --git a/library/indrec.ml b/library/indrec.ml index 251656c600..f15ed4b53f 100644 --- a/library/indrec.ml +++ b/library/indrec.ml @@ -40,10 +40,11 @@ let mis_make_case_com depopt env sigma mispec kind = | None -> mis_sort mispec <> (Prop Null) | Some d -> d in - if not (List.exists (base_sort_cmp CONV kind) (mis_kelim mispec)) then + if not (List.exists ((=) kind) (mis_kelim mispec)) then raise (InductiveError - (NotAllowedCaseAnalysis (dep,kind,mis_inductive mispec))); + (NotAllowedCaseAnalysis + (dep,(sort_of_elimination kind),mis_inductive mispec))); let nbargsprod = mis_nrealargs mispec + 1 in @@ -74,7 +75,7 @@ let mis_make_case_com depopt env sigma mispec kind = mkLambda_string "f" t (add_branch (push_rel (Anonymous, None, t) env) (k+1)) in - let typP = make_arity env' dep indf kind in + let typP = make_arity env' dep indf (sort_of_elimination kind) in it_mkLambda_or_LetIn_name env (mkLambda_string "P" typP (add_branch (push_rel (Anonymous,None,typP) env') 0)) lnamespar @@ -371,7 +372,7 @@ let mis_make_indrec env sigma listdepkind mispec = let rec put_arity env i = function | (mispeci,dep,kinds)::rest -> let indf = make_ind_family (mispeci,extended_rel_list i lnamespar) in - let typP = make_arity env dep indf kinds in + let typP = make_arity env dep indf (sort_of_elimination kinds) in mkLambda_string "P" typP (put_arity (push_rel (Anonymous,None,typP) env) (i+1) rest) | [] -> @@ -432,11 +433,12 @@ let instanciate_indrec_scheme sort = let check_arities listdepkind = List.iter - (function (mispeci,dep,kinds) -> + (function (mispeci,dep,kind) -> let id = mis_typename mispeci in let kelim = mis_kelim mispeci in - if not (List.exists (base_sort_cmp CONV kinds) kelim) then - raise (InductiveError (BadInduction (dep, id, kinds)))) + if not (List.exists ((=) kind) kelim) then + raise + (InductiveError (BadInduction (dep, id, sort_of_elimination kind)))) listdepkind let build_mutual_indrec env sigma = function @@ -459,8 +461,8 @@ let build_mutual_indrec env sigma = function | _ -> anomaly "build_indrec expects a non empty list of inductive types" let build_indrec env sigma mispec = - let kind = mis_sort mispec in - let dep = kind <> Prop Null in + let kind = elimination_of_sort (mis_sort mispec) in + let dep = kind <> ElimOnProp in List.hd (mis_make_indrec env sigma [(mispec,dep,kind)] mispec) (**********************************************************************) diff --git a/library/indrec.mli b/library/indrec.mli index e50766348b..e53b7d2a8c 100644 --- a/library/indrec.mli +++ b/library/indrec.mli @@ -21,9 +21,9 @@ open Evd (* These functions build elimination predicate for Case tactic *) -val make_case_dep : env -> 'a evar_map -> inductive -> sorts -> constr -val make_case_nodep : env -> 'a evar_map -> inductive -> sorts -> constr -val make_case_gen : env -> 'a evar_map -> inductive -> sorts -> constr +val make_case_dep : env -> 'a evar_map -> inductive -> elimination_sorts -> constr +val make_case_nodep : env -> 'a evar_map -> inductive -> elimination_sorts -> constr +val make_case_gen : env -> 'a evar_map -> inductive -> elimination_sorts -> constr (* This builds an elimination scheme associated (using the own arity of the inductive) *) @@ -34,7 +34,8 @@ val instanciate_indrec_scheme : sorts -> int -> constr -> constr (* This builds complex [Scheme] *) val build_mutual_indrec : - env -> 'a evar_map -> (inductive * bool * sorts) list -> constr list + env -> 'a evar_map -> (inductive * bool * elimination_sorts) list + -> constr list (* These are for old Case/Match typing *) |