From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 20:04:58 +0200 Subject: Remove some unused values and types --- vernac/auto_ind_decl.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'vernac/auto_ind_decl.ml') diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index b9c4c6cc5..015552d68 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -28,8 +28,6 @@ open Proofview.Notations module RelDecl = Context.Rel.Declaration -let out_punivs = Univ.out_punivs - (**********************************************************************) (* Generic synthesis of boolean equality *) -- cgit v1.2.3 From 4e84e83911c1cf7613a35b921b1e68e097f84b5a Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 20:11:47 +0200 Subject: Remove unused [open] statements --- dev/top_printers.ml | 1 - engine/eConstr.ml | 1 - engine/eConstr.mli | 1 - engine/evarutil.ml | 1 - engine/evd.ml | 4 ---- engine/proofview.mli | 1 - engine/termops.ml | 1 - engine/universes.ml | 1 - interp/constrintern.ml | 2 -- interp/constrintern.mli | 1 - interp/stdarg.ml | 2 -- interp/stdarg.mli | 1 - interp/syntax_def.ml | 2 -- intf/tactypes.mli | 1 - library/goptions.ml | 1 - library/libobject.ml | 1 - parsing/egramcoq.ml | 1 - parsing/egramcoq.mli | 8 -------- parsing/g_prim.ml4 | 1 - parsing/g_proofs.ml4 | 1 - plugins/firstorder/instances.ml | 1 - plugins/funind/functional_principles_proofs.mli | 1 - plugins/funind/g_indfun.ml4 | 1 - plugins/funind/indfun_common.ml | 1 - plugins/funind/invfun.ml | 1 - plugins/funind/merge.ml | 1 - plugins/ltac/evar_tactics.ml | 1 - plugins/ltac/extratactics.ml4 | 1 - plugins/ltac/g_auto.ml4 | 1 - plugins/ltac/g_class.ml4 | 3 --- plugins/ltac/pltac.ml | 1 - plugins/ltac/rewrite.mli | 1 - plugins/ltac/taccoerce.mli | 1 - plugins/ltac/tacentries.ml | 1 - plugins/ltac/tacenv.mli | 1 - plugins/ltac/tacinterp.ml | 1 - plugins/ltac/tacinterp.mli | 1 - plugins/ltac/tactic_debug.mli | 1 - plugins/micromega/coq_micromega.ml | 1 - plugins/nsatz/ideal.ml | 2 -- plugins/setoid_ring/newring.ml | 1 - plugins/setoid_ring/newring.mli | 3 --- plugins/ssrmatching/ssrmatching.ml4 | 14 -------------- plugins/ssrmatching/ssrmatching.mli | 1 - pretyping/cbv.mli | 1 - pretyping/classops.ml | 1 - pretyping/classops.mli | 1 - pretyping/coercion.ml | 1 - pretyping/coercion.mli | 1 - pretyping/detyping.ml | 1 - pretyping/evarconv.ml | 1 - pretyping/evarconv.mli | 1 - pretyping/evardefine.ml | 1 - pretyping/find_subterm.mli | 1 - pretyping/inductiveops.ml | 1 - pretyping/patternops.ml | 1 - pretyping/patternops.mli | 1 - pretyping/pretype_errors.ml | 1 - pretyping/pretyping.ml | 1 - pretyping/program.ml | 1 - pretyping/tacred.mli | 1 - pretyping/typeclasses_errors.ml | 1 - pretyping/typeclasses_errors.mli | 1 - printing/prettyp.mli | 1 - proofs/clenvtac.mli | 1 - proofs/goal.ml | 1 - proofs/proof_type.mli | 3 --- proofs/refiner.ml | 1 - proofs/tacmach.mli | 1 - stm/stm.mli | 3 --- tactics/auto.ml | 1 - tactics/auto.mli | 1 - tactics/btermdn.mli | 1 - tactics/class_tactics.ml | 3 --- tactics/class_tactics.mli | 1 - tactics/contradiction.mli | 1 - tactics/eauto.mli | 2 -- tactics/elim.ml | 1 - tactics/elim.mli | 1 - tactics/eqdecide.ml | 1 - tactics/equality.ml | 1 - tactics/equality.mli | 1 - tactics/hints.mli | 1 - tactics/hipattern.mli | 1 - tactics/inv.ml | 1 - tactics/inv.mli | 1 - tactics/leminv.mli | 1 - tactics/tactics.ml | 2 -- toplevel/coqloop.mli | 2 -- vernac/auto_ind_decl.ml | 2 -- vernac/classes.ml | 2 -- vernac/obligations.mli | 1 - vernac/search.ml | 2 -- vernac/search.mli | 1 - 94 files changed, 137 deletions(-) (limited to 'vernac/auto_ind_decl.ml') diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 918e98f77..7caaf2d9d 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -503,7 +503,6 @@ VERNAC COMMAND EXTEND PrintConstr END *) -open Pcoq open Genarg open Stdarg open Egramml diff --git a/engine/eConstr.ml b/engine/eConstr.ml index bb9075e74..54d3ce6cf 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open CSig open CErrors open Util open Names diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 3a9469e55..693b592fd 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -9,7 +9,6 @@ open CSig open Names open Constr -open Context open Environ type t diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 1624dc93e..fba466107 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -10,7 +10,6 @@ open CErrors open Util open Names open Term -open Vars open Termops open Namegen open Pre_env diff --git a/engine/evd.ml b/engine/evd.ml index 5419a10a8..6b1e1a855 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -14,8 +14,6 @@ open Nameops open Term open Vars open Environ -open Globnames -open Context.Named.Declaration module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration @@ -360,8 +358,6 @@ module EvMap = Evar.Map module EvNames : sig -open Misctypes - type t val empty : t diff --git a/engine/proofview.mli b/engine/proofview.mli index a3b0304b1..da8a8fecd 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -13,7 +13,6 @@ state and returning a value of type ['a]. *) open Util -open Term open EConstr (** Main state of tactics *) diff --git a/engine/termops.ml b/engine/termops.ml index 29dcddbb0..19e62f8e6 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1427,7 +1427,6 @@ let dependency_closure env sigma sign hyps = List.rev lh let global_app_of_constr sigma c = - let open Univ in let open Globnames in match EConstr.kind sigma c with | Const (c, u) -> (ConstRef c, u), None diff --git a/engine/universes.ml b/engine/universes.ml index ab561784c..1900112dd 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -13,7 +13,6 @@ open Term open Environ open Univ open Globnames -open Decl_kinds let pr_with_global_universes l = try Nameops.pr_id (LMap.find l (snd (Global.global_universe_names ()))) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d75487ecf..389880c5c 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2045,8 +2045,6 @@ let interp_binder_evars env evdref na t = let t' = locate_if_hole (loc_of_glob_constr t) na t in understand_tcc_evars env evdref ~expected_type:IsType t' -open Environ - let my_intern_constr env lvar acc c = internalize env acc false lvar c diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 758d4e650..fdd50c6a1 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -18,7 +18,6 @@ open Constrexpr open Notation_term open Pretyping open Misctypes -open Decl_kinds (** Translation from front abstract syntax of term to untyped terms (glob_constr) *) diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 341ff5662..5920b0d50 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -6,9 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Loc open Misctypes -open Tactypes open Genarg open Geninterp diff --git a/interp/stdarg.mli b/interp/stdarg.mli index 113fe40ba..ac40a2328 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -10,7 +10,6 @@ open Loc open Names -open Term open EConstr open Libnames open Globnames diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index c3f4c4f30..ed7b0b70d 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -106,5 +106,3 @@ let search_syntactic_definition kn = let def = out_pat pat in verbose_compat kn def v; def - -open Goptions diff --git a/intf/tactypes.mli b/intf/tactypes.mli index 02cfc44e2..ef90b911c 100644 --- a/intf/tactypes.mli +++ b/intf/tactypes.mli @@ -13,7 +13,6 @@ open Loc open Names open Constrexpr -open Glob_term open Pattern open Misctypes diff --git a/library/goptions.ml b/library/goptions.ml index 1c08b9539..c111113ca 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -235,7 +235,6 @@ with Not_found -> then error "Sorry, this option name is already used." open Libobject -open Lib let warn_deprecated_option = CWarnings.create ~name:"deprecated-option" ~category:"deprecated" diff --git a/library/libobject.ml b/library/libobject.ml index 8757ca08c..897591762 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -8,7 +8,6 @@ open Libnames open Pp -open Util module Dyn = Dyn.Make(struct end) diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 65e99d1b9..86c66ec5f 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -10,7 +10,6 @@ open CErrors open Util open Pcoq open Constrexpr -open Notation open Notation_term open Extend open Libnames diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 6dda3817a..0a0430ba6 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -6,14 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names -open Constrexpr -open Notation_term -open Pcoq -open Extend -open Genarg -open Egramml - (** Mapping of grammar productions to camlp4 actions *) (** This is the part specific to Coq-level Notation and Tactic Notation. diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 2af4ed533..abb463f82 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -8,7 +8,6 @@ open Names open Libnames -open Tok (* necessary for camlp4 *) open Pcoq open Pcoq.Prim diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 7ca2e4a4f..68b8be6b8 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -9,7 +9,6 @@ open Constrexpr open Vernacexpr open Misctypes -open Tok open Pcoq open Pcoq.Prim diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 62f811546..2b624b983 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -17,7 +17,6 @@ open Tacmach.New open Tactics open Tacticals.New open Proofview.Notations -open Termops open Reductionops open Formula open Sequent diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli index 7ddc84d01..61752aa33 100644 --- a/plugins/funind/functional_principles_proofs.mli +++ b/plugins/funind/functional_principles_proofs.mli @@ -1,5 +1,4 @@ open Names -open Term val prove_princ_for_struct : Evd.evar_map ref -> diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 0dccd25d7..b5eacee81 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) open Ltac_plugin open Util -open Term open Pp open Constrexpr open Indfun_common diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 7b0d7d27d..c6f5c2745 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -508,7 +508,6 @@ let list_rewrite (rev:bool) (eqs: (EConstr.constr*bool) list) = (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));; let decompose_lam_n sigma n = - let open EConstr in if n < 0 then CErrors.error "decompose_lam_n: integer parameter must be positive"; let rec lamdec_rec l n c = if Int.equal n 0 then l,c diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 94ec0a898..29472cdef 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -7,7 +7,6 @@ (************************************************************************) open Ltac_plugin -open Tacexpr open Declarations open CErrors open Util diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index f1ca57585..0af0898a0 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -19,7 +19,6 @@ open Pp open Names open Term open Vars -open Termops open Declarations open Glob_term open Glob_termops diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 5d3f6df03..bc9c300e2 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -9,7 +9,6 @@ open Util open Names open Term -open EConstr open CErrors open Evar_refiner open Tacmach diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 35cfe8b54..21419d1f9 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -21,7 +21,6 @@ open Tacexpr open Glob_ops open CErrors open Util -open Evd open Termops open Equality open Misctypes diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index dfa8331ff..50e8255a6 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -16,7 +16,6 @@ open Pcoq.Constr open Pltac open Hints open Tacexpr -open Proofview.Notations open Names DECLARE PLUGIN "g_auto" diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 index ff5e7d5ff..23ce368ee 100644 --- a/plugins/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.ml4 @@ -8,9 +8,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Misctypes open Class_tactics -open Pltac open Stdarg open Tacarg open Names @@ -95,7 +93,6 @@ END (** TODO: DEPRECATE *) (* A progress test that allows to see if the evars have changed *) open Term -open Proofview.Goal open Proofview.Notations let rec eq_constr_mod_evars sigma x y = diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml index 1d21118ae..7e979d269 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Pcoq (* Main entry for extensions *) diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 7a20838a2..6683d753b 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -14,7 +14,6 @@ open Constrexpr open Tacexpr open Misctypes open Evd -open Proof_type open Tacinterp (** TODO: document and clean me! *) diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index 9c4ac5265..4a44f86d9 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -8,7 +8,6 @@ open Util open Names -open Term open EConstr open Misctypes open Pattern diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index ef1d69d35..32750383b 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -15,7 +15,6 @@ open Genarg open Extend open Pcoq open Egramml -open Egramcoq open Vernacexpr open Libnames open Nameops diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli index 94e14223a..d1e2a7bbe 100644 --- a/plugins/ltac/tacenv.mli +++ b/plugins/ltac/tacenv.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Genarg open Names open Tacexpr open Geninterp diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index fcdf7bb2c..b8c021f18 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -25,7 +25,6 @@ open Refiner open Tacmach.New open Tactic_debug open Constrexpr -open Term open Termops open Tacexpr open Genarg diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 1e5f6bd42..494f36a95 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -8,7 +8,6 @@ open Names open Tactic_debug -open Term open EConstr open Tacexpr open Genarg diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index 7745d9b7b..0b4d35a22 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -10,7 +10,6 @@ open Environ open Pattern open Names open Tacexpr -open Term open EConstr open Evd diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index eb26c5431..a36607ec3 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -331,7 +331,6 @@ module M = struct open Coqlib - open Term open Constr open EConstr diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml index 41f2edfcf..a120d4efb 100644 --- a/plugins/nsatz/ideal.ml +++ b/plugins/nsatz/ideal.ml @@ -196,8 +196,6 @@ module Hashpol = Hashtbl.Make( (* A pretty printer for polynomials, with Maple-like syntax. *) -open Format - let getvar lv i = try (List.nth lv i) with Failure _ -> (List.fold_left (fun r x -> r^" "^x) "lv= " lv) diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 6e072e831..d59ffee54 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -19,7 +19,6 @@ open Environ open Libnames open Globnames open Glob_term -open Tacticals open Tacexpr open Coqlib open Mod_subst diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli index 4367d021c..d9d32c681 100644 --- a/plugins/setoid_ring/newring.mli +++ b/plugins/setoid_ring/newring.mli @@ -7,13 +7,10 @@ (************************************************************************) open Names -open Constr open EConstr open Libnames open Globnames open Constrexpr -open Tacexpr -open Proof_type open Newring_ast val protect_tac_in : string -> Id.t -> unit Proofview.tactic diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index f146fbb11..72c70750c 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -21,30 +21,21 @@ open Pp open Pcoq open Genarg open Stdarg -open Tacarg open Term open Vars -open Topconstr open Libnames open Tactics open Tacticals open Termops -open Namegen open Recordops open Tacmach -open Coqlib open Glob_term open Util open Evd -open Extend -open Goptions open Tacexpr -open Proofview.Notations open Tacinterp open Pretyping open Constr -open Pltac -open Extraargs open Ppconstr open Printer @@ -54,14 +45,9 @@ open Decl_kinds open Evar_kinds open Constrexpr open Constrexpr_ops -open Notation_term -open Notation_ops -open Locus -open Locusops DECLARE PLUGIN "ssrmatching_plugin" -type loc = Loc.t let dummy_loc = Loc.ghost let errorstrm = CErrors.user_err ~hdr:"ssrmatching" let loc_error loc msg = CErrors.user_err ~loc ~hdr:msg (str msg) diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 1f984b160..638b4e254 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -4,7 +4,6 @@ open Genarg open Tacexpr open Environ -open Tacmach open Evd open Proof_type open Term diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index b014af2c7..eb25994be 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open EConstr open Environ open CClosure diff --git a/pretyping/classops.ml b/pretyping/classops.ml index e9b3d197b..32da81f96 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -17,7 +17,6 @@ open Nametab open Environ open Libobject open Term -open Termops open Mod_subst (* usage qque peu general: utilise aussi dans record *) diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 0d741a5a5..c4238e8b0 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open Environ open EConstr open Evd diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 542db7fdf..c26e7458e 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -22,7 +22,6 @@ open Environ open EConstr open Vars open Reductionops -open Typeops open Pretype_errors open Classops open Evarutil diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index bc63d092d..ea3d3f0fa 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -8,7 +8,6 @@ open Evd open Names -open Term open Environ open EConstr open Glob_term diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 8ba408679..483e2b432 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -13,7 +13,6 @@ open CErrors open Util open Names open Term -open Environ open EConstr open Vars open Inductiveops diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 4bb66b8e9..305eae15a 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -21,7 +21,6 @@ open Recordops open Evarutil open Evardefine open Evarsolve -open Globnames open Evd open Pretype_errors open Sigma.Notations diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index fc07f0fbe..7cee1e8a7 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open EConstr open Environ open Reductionops diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index c5ae684e3..5fd104c78 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -11,7 +11,6 @@ open Pp open Names open Term open Termops -open Environ open EConstr open Vars open Namegen diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli index e3d3b74f1..d22f94e4e 100644 --- a/pretyping/find_subterm.mli +++ b/pretyping/find_subterm.mli @@ -7,7 +7,6 @@ (************************************************************************) open Locus -open Term open Evd open Pretype_errors open Environ diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 5b42add28..429e5005e 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -459,7 +459,6 @@ let extract_mrectype sigma t = | _ -> raise Not_found let find_mrectype_vect env sigma c = - let open EConstr in let (t, l) = Termops.decompose_app_vect sigma (whd_all env sigma c) in match EConstr.kind sigma t with | Ind ind -> (ind, l) diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index b16d04495..33a68589c 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -20,7 +20,6 @@ open Mod_subst open Misctypes open Decl_kinds open Pattern -open Evd open Environ let case_info_pattern_eq i1 i2 = diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 5694d345c..791fd74ed 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term open EConstr open Globnames open Glob_term diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 24f6d1689..f9cf6b83b 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util open Names open Term open Environ diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 497bde340..68ef97659 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -33,7 +33,6 @@ open EConstr open Vars open Reductionops open Type_errors -open Typeops open Typing open Globnames open Nameops diff --git a/pretyping/program.ml b/pretyping/program.ml index caa5a5c8a..42acc5705 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -10,7 +10,6 @@ open Pp open CErrors open Util open Names -open Term let make_dir l = DirPath.make (List.rev_map Id.of_string l) diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 76d0bc241..c31212e26 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open Environ open Evd open EConstr diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index 2db0e9e88..754dacd19 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -8,7 +8,6 @@ (*i*) open Names -open Term open EConstr open Environ open Constrexpr diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index 9bd430e4d..558575ccc 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -8,7 +8,6 @@ open Loc open Names -open Term open EConstr open Environ open Constrexpr diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 38e111034..6841781cc 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -8,7 +8,6 @@ open Pp open Names -open Term open Environ open Reductionops open Libnames diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index 5b7164705..26069207e 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -8,7 +8,6 @@ (** Legacy components of the previous proof engine. *) -open Term open Clenv open EConstr open Unification diff --git a/proofs/goal.ml b/proofs/goal.ml index 9046f4534..fc8e635a0 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -8,7 +8,6 @@ open Util open Pp -open Term open Sigma.Notations module NamedDecl = Context.Named.Declaration diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 03bc5e471..e59db9e42 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -11,9 +11,6 @@ open Evd open Names open Term -open Glob_term -open Nametab -open Misctypes (** This module defines the structure of proof tree and the tactic type. So, it is used by [Proof_tree] and [Refiner] *) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index bc12b3ba7..259e96a27 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -10,7 +10,6 @@ open Pp open CErrors open Util open Evd -open Environ open Proof_type open Logic diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 627a8e0e7..e6e60e27f 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -15,7 +15,6 @@ open Proof_type open Redexpr open Pattern open Locus -open Misctypes (** Operations for handling terms under a local typing context. *) diff --git a/stm/stm.mli b/stm/stm.mli index 30e9629c6..d2bee4496 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -6,10 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Vernacexpr open Names -open Feedback -open Loc (** state-transaction-machine interface *) diff --git a/tactics/auto.ml b/tactics/auto.ml index 42230dff1..324c551d0 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -12,7 +12,6 @@ open Pp open Util open CErrors open Names -open Vars open Termops open EConstr open Environ diff --git a/tactics/auto.mli b/tactics/auto.mli index 32710e347..9ed9f0ae2 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -9,7 +9,6 @@ (** This files implements auto and related automation tactics *) open Names -open Term open EConstr open Clenv open Pattern diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index 2a5e7c345..27f624f71 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term open Pattern open Names diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index c430e776a..6c724a1eb 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -18,7 +18,6 @@ open Names open Term open Termops open EConstr -open Reduction open Proof_type open Tacticals open Tacmach @@ -1219,7 +1218,6 @@ module Search = struct let intro_tac info kont gl = let open Proofview in - let open Proofview.Notations in let env = Goal.env gl in let sigma = Goal.sigma gl in let s = Sigma.to_evar_map sigma in @@ -1257,7 +1255,6 @@ module Search = struct let search_tac_gl ?st only_classes dep hints depth i sigma gls gl : unit Proofview.tactic = let open Proofview in - let open Proofview.Notations in if false (* In 8.6, still allow non-class goals only_classes && not (is_class_type sigma (Goal.concl gl)) *) then Tacticals.New.tclZEROMSG (str"Not a subgoal for a class") else diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index 738cc0feb..4ab29f260 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -9,7 +9,6 @@ (** This files implements typeclasses eauto *) open Names -open Constr open EConstr open Tacmach diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli index 510b135b0..2cf5a6829 100644 --- a/tactics/contradiction.mli +++ b/tactics/contradiction.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term open EConstr open Misctypes diff --git a/tactics/eauto.mli b/tactics/eauto.mli index e2006ac1e..c952f4e72 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -6,9 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term open EConstr -open Proof_type open Hints open Tactypes diff --git a/tactics/elim.ml b/tactics/elim.ml index e37ec6bce..855cb206f 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -8,7 +8,6 @@ open Util open Names -open Term open Termops open EConstr open Inductiveops diff --git a/tactics/elim.mli b/tactics/elim.mli index dc1af79ba..fb7cc7b83 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open EConstr open Tacticals open Misctypes diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index bac3980d2..5012b0ef7 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -25,7 +25,6 @@ open Constr_matching open Misctypes open Tactypes open Hipattern -open Pretyping open Proofview.Notations open Tacmach.New open Coqlib diff --git a/tactics/equality.ml b/tactics/equality.ml index 25c28cf4a..cc7701ad5 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -14,7 +14,6 @@ open Names open Nameops open Term open Termops -open Environ open EConstr open Vars open Namegen diff --git a/tactics/equality.mli b/tactics/equality.mli index 5467b4af2..d979c580a 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -8,7 +8,6 @@ (*i*) open Names -open Term open Evd open EConstr open Environ diff --git a/tactics/hints.mli b/tactics/hints.mli index 467fd46d5..3a0339ff5 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -9,7 +9,6 @@ open Pp open Util open Names -open Term open EConstr open Environ open Globnames diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index dd09c3a4d..82a3d47b5 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open Evd open EConstr open Coqlib diff --git a/tactics/inv.ml b/tactics/inv.ml index 904a17417..266cac5c7 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -13,7 +13,6 @@ open Names open Nameops open Term open Termops -open Environ open EConstr open Vars open Namegen diff --git a/tactics/inv.mli b/tactics/inv.mli index 446a62f6d..5835e763d 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open EConstr open Misctypes open Tactypes diff --git a/tactics/leminv.mli b/tactics/leminv.mli index 26d4ac994..a343fc81a 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open EConstr open Constrexpr open Misctypes diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 53f8e4d5f..f3f7d16b7 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5037,8 +5037,6 @@ end (** Tacticals defined directly in term of Proofview *) module New = struct - open Proofview.Notations - open Genredexpr open Locus diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 66bbf43f6..13e860a88 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp - (** The Coq toplevel loop. *) (** A buffer for the character read from a channel. We store the command diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 015552d68..25091f783 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -9,7 +9,6 @@ (* This file is about the automatic generation of schemes about decidable equality, created by Vincent Siles, Oct 2007 *) -open Tacmach open CErrors open Util open Pp @@ -716,7 +715,6 @@ let compute_lb_goal ind lnamesparrec nparrec = ))), eff let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = - let open EConstr in let list_id = list_id lnamesparrec in let avoid = ref [] in let first_intros = diff --git a/vernac/classes.ml b/vernac/classes.ml index 833719965..d515b0c9b 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -66,8 +66,6 @@ let _ = Hook.set Typeclasses.classes_transparent_state_hook (fun () -> Hints.Hint_db.transparent_state (Hints.searchtable_map typeclasses_db)) -open Vernacexpr - (** TODO: add subinstances *) let existing_instance glob g info = let c = global g in diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 11366fe91..a276f9f9a 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -12,7 +12,6 @@ open Evd open Names open Pp open Globnames -open Vernacexpr open Decl_kinds (** Forward declaration. *) diff --git a/vernac/search.ml b/vernac/search.ml index 6279b17ae..5b6e9a9c3 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -14,11 +14,9 @@ open Declarations open Libobject open Environ open Pattern -open Printer open Libnames open Globnames open Nametab -open Goptions module NamedDecl = Context.Named.Declaration diff --git a/vernac/search.mli b/vernac/search.mli index 82b79f75d..e34522d8a 100644 --- a/vernac/search.mli +++ b/vernac/search.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names open Term open Environ -- cgit v1.2.3 From d0252cac3167ef1e5cd26c1b9b40aea06d343413 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 1 May 2017 17:48:57 +0200 Subject: More consistent writing of de Bruijn. --- checker/term.ml | 4 ++-- dev/doc/cic.dtd | 2 +- doc/RecTutorial/coqartmacros.tex | 2 +- doc/refman/RefMan-tus.tex | 18 +++++++++--------- engine/evarutil.ml | 2 +- kernel/constr.ml | 2 +- kernel/constr.mli | 2 +- kernel/nativeconv.ml | 2 +- kernel/term.ml | 2 +- kernel/term.mli | 2 +- kernel/vars.ml | 2 +- kernel/vars.mli | 4 ++-- tactics/dnet.mli | 2 +- vernac/auto_ind_decl.ml | 4 ++-- vernac/obligations.ml | 6 +++--- 15 files changed, 28 insertions(+), 28 deletions(-) (limited to 'vernac/auto_ind_decl.ml') diff --git a/checker/term.ml b/checker/term.ml index 591348cb6..24e6008d3 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* This module instantiates the structure of generic deBruijn terms to Coq *) +(* This module instantiates the structure of generic de Bruijn terms to Coq *) open CErrors open Util @@ -94,7 +94,7 @@ let closedn n c = in try closed_rec n c; true with LocalOccur -> false -(* [closed0 M] is true iff [M] is a (deBruijn) closed term *) +(* [closed0 M] is true iff [M] is a (de Bruijn) closed term *) let closed0 = closedn 0 diff --git a/dev/doc/cic.dtd b/dev/doc/cic.dtd index 7a9d7eb1e..cc33efd48 100644 --- a/dev/doc/cic.dtd +++ b/dev/doc/cic.dtd @@ -125,7 +125,7 @@ id ID #REQUIRED sort %sort; #REQUIRED> - + diff --git a/doc/RecTutorial/coqartmacros.tex b/doc/RecTutorial/coqartmacros.tex index 2a2c21196..72d749269 100644 --- a/doc/RecTutorial/coqartmacros.tex +++ b/doc/RecTutorial/coqartmacros.tex @@ -149,7 +149,7 @@ \newcommand{\PicAbst}[3]{\begin{bundle}{\bf abst}\chunk{#1}\chunk{#2}\chunk{#3}% \end{bundle}} -% the same in DeBruijn form +% the same in de Bruijn form \newcommand{\PicDbj}[2]{\begin{bundle}{\bf abst}\chunk{#1}\chunk{#2} \end{bundle}} diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex index c55b3775c..017de6d48 100644 --- a/doc/refman/RefMan-tus.tex +++ b/doc/refman/RefMan-tus.tex @@ -288,8 +288,8 @@ constructors: \item $(\texttt{VAR}\;id)$, a reference to a global identifier called $id$; \item $(\texttt{Rel}\;n)$, a bound variable, whose binder is the $nth$ binder up in the term; -\item $\texttt{DLAM}\;(x,t)$, a deBruijn's binder on the term $t$; -\item $\texttt{DLAMV}\;(x,vt)$, a deBruijn's binder on all the terms of +\item $\texttt{DLAM}\;(x,t)$, a de Bruijn's binder on the term $t$; +\item $\texttt{DLAMV}\;(x,vt)$, a de Bruijn's binder on all the terms of the vector $vt$; \item $(\texttt{DOP0}\;op)$, a unary operator $op$; \item $\texttt{DOP2}\;(op,t_1,t_2)$, the application of a binary @@ -299,7 +299,7 @@ vector of terms $vt$. \end{itemize} In this meta-language, bound variables are represented using the -so-called deBruijn's indexes. In this representation, an occurrence of +so-called de Bruijn's indexes. In this representation, an occurrence of a bound variable is denoted by an integer, meaning the number of binders that must be traversed to reach its own binder\footnote{Actually, $(\texttt{Rel}\;n)$ means that $(n-1)$ binders @@ -339,7 +339,7 @@ on the terms of the meta-language: \fun{val Generic.dependent : 'op term -> 'op term -> bool} {Returns true if the first term is a sub-term of the second.} %\fun{val Generic.subst\_var : identifier -> 'op term -> 'op term} -% { $(\texttt{subst\_var}\;id\;t)$ substitutes the deBruijn's index +% { $(\texttt{subst\_var}\;id\;t)$ substitutes the de Bruijn's index % associated to $id$ to every occurrence of the term % $(\texttt{VAR}\;id)$ in $t$.} \end{description} @@ -482,7 +482,7 @@ following constructor functions: \begin{description} \fun{val Term.mkRel : int -> constr} - {$(\texttt{mkRel}\;n)$ represents deBruijn's index $n$.} + {$(\texttt{mkRel}\;n)$ represents de Bruijn's index $n$.} \fun{val Term.mkVar : identifier -> constr} {$(\texttt{mkVar}\;id)$ @@ -545,7 +545,7 @@ following constructor functions: \fun{val Term.mkProd : name ->constr ->constr -> constr} {$(\texttt{mkProd}\;x\;A\;B)$ represents the product $(x:A)B$. - The free ocurrences of $x$ in $B$ are represented by deBruijn's + The free ocurrences of $x$ in $B$ are represented by de Bruijn's indexes.} \fun{val Term.mkNamedProd : identifier -> constr -> constr -> constr} @@ -553,14 +553,14 @@ following constructor functions: but the bound occurrences of $x$ in $B$ are denoted by the identifier $(\texttt{mkVar}\;x)$. The function automatically changes each occurrences of this identifier into the corresponding - deBruijn's index.} + de Bruijn's index.} \fun{val Term.mkArrow : constr -> constr -> constr} {$(\texttt{arrow}\;A\;B)$ represents the type $(A\rightarrow B)$.} \fun{val Term.mkLambda : name -> constr -> constr -> constr} {$(\texttt{mkLambda}\;x\;A\;b)$ represents the lambda abstraction - $[x:A]b$. The free ocurrences of $x$ in $B$ are represented by deBruijn's + $[x:A]b$. The free ocurrences of $x$ in $B$ are represented by de Bruijn's indexes.} \fun{val Term.mkNamedLambda : identifier -> constr -> constr -> constr} @@ -666,7 +666,7 @@ use the primitive \textsl{Case} described in Chapter \ref{Cic} \item Restoring type coercions and synthesizing the implicit arguments (the one denoted by question marks in {\Coq} syntax: see Section~\ref{Coercions}). -\item Transforming the named bound variables into deBruijn's indexes. +\item Transforming the named bound variables into de Bruijn's indexes. \item Classifying the global names into the different classes of constants (defined constants, constructors, inductive types, etc). \end{enumerate} diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 1624dc93e..22f93faa6 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -462,7 +462,7 @@ let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?nami ev (* This assumes an evar with identity instance and generalizes it over only - the De Bruijn part of the context *) + the de Bruijn part of the context *) let generalize_evar_over_rels sigma (ev,args) = let open EConstr in let evi = Evd.find sigma ev in diff --git a/kernel/constr.ml b/kernel/constr.ml index 49e17d74d..ae58fd068 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -124,7 +124,7 @@ type types = constr (* Term constructors *) (*********************) -(* Constructs a DeBruijn index with number n *) +(* Constructs a de Bruijn index with number n *) let rels = [|Rel 1;Rel 2;Rel 3;Rel 4;Rel 5;Rel 6;Rel 7; Rel 8; Rel 9;Rel 10;Rel 11;Rel 12;Rel 13;Rel 14;Rel 15; Rel 16|] diff --git a/kernel/constr.mli b/kernel/constr.mli index d90afea8f..e0954160f 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -70,7 +70,7 @@ type types = constr (** {6 Term constructors. } *) -(** Constructs a DeBruijn index (DB indices begin at 1) *) +(** Constructs a de Bruijn index (DB indices begin at 1) *) val mkRel : int -> constr (** Constructs a Variable *) diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 3c0afe380..3593d94c2 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -141,7 +141,7 @@ let native_conv_gen pb sigma env univs t1 t2 = let t1 = Sys.time () in let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in if !Flags.debug then Feedback.msg_debug (Pp.str time_info); - (* TODO change 0 when we can have deBruijn *) + (* TODO change 0 when we can have de Bruijn *) fst (conv_val env pb 0 !rt1 !rt2 univs) end | _ -> anomaly (Pp.str "Compilation failure") diff --git a/kernel/term.ml b/kernel/term.ml index 7c6136f08..03562d9f3 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -169,7 +169,7 @@ let hcons_types = Constr.hcons exception DestKO -(* Destructs a DeBruijn index *) +(* Destructs a de Bruijn index *) let destRel c = match kind_of_term c with | Rel n -> n | _ -> raise DestKO diff --git a/kernel/term.mli b/kernel/term.mli index 623d2c8a6..241ef322f 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -127,7 +127,7 @@ val is_small : sorts -> bool exception DestKO -(** Destructs a DeBruijn index *) +(** Destructs a de Bruijn index *) val destRel : constr -> int (** Destructs an existential variable *) diff --git a/kernel/vars.ml b/kernel/vars.ml index 4affb5f9f..f1c0a4f08 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -27,7 +27,7 @@ let closedn n c = in try closed_rec n c; true with LocalOccur -> false -(* [closed0 M] is true iff [M] is a (deBruijn) closed term *) +(* [closed0 M] is true iff [M] is a (de Bruijn) closed term *) let closed0 c = closedn 0 c diff --git a/kernel/vars.mli b/kernel/vars.mli index adeac422e..df5c55118 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -11,10 +11,10 @@ open Constr (** {6 Occur checks } *) -(** [closedn n M] is true iff [M] is a (deBruijn) closed term under n binders *) +(** [closedn n M] is true iff [M] is a (de Bruijn) closed term under n binders *) val closedn : int -> constr -> bool -(** [closed0 M] is true iff [M] is a (deBruijn) closed term *) +(** [closed0 M] is true iff [M] is a (de Bruijn) closed term *) val closed0 : constr -> bool (** [noccurn n M] returns true iff [Rel n] does NOT occur in term [M] *) diff --git a/tactics/dnet.mli b/tactics/dnet.mli index 9f29c60b6..565a916f8 100644 --- a/tactics/dnet.mli +++ b/tactics/dnet.mli @@ -26,7 +26,7 @@ distincts, or you'll get unexpected behaviours. Warning 2: This structure is perfect, i.e. the set of candidates - returned is equal to the set of solutions. Beware of DeBruijn + returned is equal to the set of solutions. Beware of de Bruijn shifts and sorts subtyping though (which makes the comparison not symmetric, see term_dnet.ml). diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index b9c4c6cc5..c91dcc505 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -95,7 +95,7 @@ let destruct_on_using c id = let destruct_on_as c l = destruct false None c (Some (dl,l)) None -(* reconstruct the inductive with the correct deBruijn indexes *) +(* reconstruct the inductive with the correct de Bruijn indexes *) let mkFullInd (ind,u) n = let mib = Global.lookup_mind (fst ind) in let nparams = mib.mind_nparams in @@ -174,7 +174,7 @@ let build_beq_scheme mode kn = (* give a type A, this function tries to find the equality on A declared previously *) (* nlist = the number of args (A , B , ... ) - eqA = the deBruijn index of the first eq param + eqA = the de Bruijn index of the first eq param ndx = how much to translate due to the 2nd Case *) let compute_A_equality rel_list nlist eqA ndx t = diff --git a/vernac/obligations.ml b/vernac/obligations.ml index ea2401b5c..e0520216b 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -8,7 +8,7 @@ open Declare (** - Get types of existentials ; - Flatten dependency tree (prefix order) ; - - Replace existentials by De Bruijn indices in term, applied to the right arguments ; + - Replace existentials by de Bruijn indices in term, applied to the right arguments ; - Apply term prefixed by quantification on "existentials". *) @@ -51,7 +51,7 @@ type oblinfo = ev_tac: unit Proofview.tactic option; ev_deps: Int.Set.t } -(** Substitute evar references in t using De Bruijn indices, +(** Substitute evar references in t using de Bruijn indices, where n binders were passed through. *) let subst_evar_constr evs n idf t = @@ -102,7 +102,7 @@ let subst_evar_constr evs n idf t = t', !seen, !transparent -(** Substitute variable references in t using De Bruijn indices, +(** Substitute variable references in t using de Bruijn indices, where n binders were passed through. *) let subst_vars acc n t = let var_index id = Util.List.index Id.equal id acc in -- cgit v1.2.3