diff options
| author | Pierre-Marie Pédrot | 2014-06-17 14:26:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-06-17 15:44:38 +0200 |
| commit | 90d64647d3fd5dbf5c337944dc0038f0b19b8a51 (patch) | |
| tree | b33528c72730ec541a75e3d0baaead6789f4dcb9 /toplevel/command.ml | |
| parent | d412844753ef25f4431c209f47b97b9fa498297d (diff) | |
Removing dead code.
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index d28445f177..13696a17c1 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -228,9 +228,6 @@ let declare_assumption is_coe (local,p,kind) (c,ctx) imps impl nl (_,ident) = ma in (gr,inst,Lib.is_modtype_strict ()) -let declare_assumptions_hook = ref ignore -let set_declare_assumptions_hook = (:=) declare_assumptions_hook - let interp_assumption evdref env bl c = let c = prod_constr_expr c bl in let ty, impls = interp_type_evars_impls evdref env c in @@ -585,9 +582,6 @@ type one_inductive_impls = Impargs.manual_explicitation list (* for inds *)* Impargs.manual_explicitation list list (* for constrs *) -type one_inductive_expr = - lident * local_binder list * constr_expr option * constructor_expr list - let do_mutual_inductive indl poly prv finite = let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in (* Interpret the types *) @@ -1079,11 +1073,6 @@ let out_def = function | Some def -> def | None -> error "Program Fixpoint needs defined bodies." -let collect_evars_of_term evd c ty = - let evars = Evar.Set.union (evars_of_term c) (evars_of_term ty) in - Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev)) - evars Evd.empty - let do_program_recursive local p fixkind fixl ntns = let isfix = fixkind != Obligations.IsCoFixpoint in let (env, rec_sign, evd), fix, info = |