diff options
69 files changed, 71 insertions, 91 deletions
diff --git a/kernel/abstraction.ml b/kernel/abstraction.ml index a6e5937a4..04ed64992 100644 --- a/kernel/abstraction.ml +++ b/kernel/abstraction.ml @@ -3,7 +3,7 @@ open Util open Names -(*i open Generic i*) +(* open Generic *) open Term type abstraction_body = { diff --git a/kernel/closure.mli b/kernel/closure.mli index 940cd2664..d9353abfa 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -4,7 +4,7 @@ (*i*) open Pp open Names -(*i open Generic i*) +(* open Generic *) open Term open Evd open Environ diff --git a/kernel/declarations.ml b/kernel/declarations.ml index a5cb164d0..9c6ffb172 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -3,7 +3,7 @@ open Names open Univ -(*i open Generic i*) +(* open Generic *) open Term open Sign diff --git a/kernel/environ.ml b/kernel/environ.ml index 604d0aea3..257cba2b1 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -6,7 +6,7 @@ open Util open Names open Sign open Univ -(*i open Generic i*) +(* open Generic *) open Term open Declarations open Abstraction @@ -310,21 +310,7 @@ let make_all_name_different env = push_rel (Name id,c,t) newenv) env -(* Abstractions. *) -(* -let evaluable_abst env = function - | DOPN (Abst _,_) -> true - | _ -> invalid_arg "evaluable_abst" - -let translucent_abst env = function - | DOPN (Abst _,_) -> false - | _ -> invalid_arg "translucent_abst" - -let abst_value env = function - | DOPN(Abst sp, args) -> - contract_abstraction (lookup_abst sp env) args - | _ -> invalid_arg "abst_value" -*) +(* Constants *) let defined_constant env = function | DOPN (Const sp, _) -> is_defined (lookup_constant sp env) | _ -> invalid_arg "defined_constant" diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index a37e469bd..534a95c94 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -3,7 +3,7 @@ open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Declarations open Inductive diff --git a/kernel/inductive.ml b/kernel/inductive.ml index db3329a1a..569b681e9 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -4,7 +4,7 @@ open Util open Names open Univ -(*i open Generic i*) +(* open Generic *) open Term open Sign open Declarations diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml index 9b1d9289a..ed625a22f 100644 --- a/kernel/instantiate.ml +++ b/kernel/instantiate.ml @@ -4,7 +4,7 @@ open Pp open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Sign open Evd diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 352e41e38..0d88ccc73 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -4,7 +4,7 @@ open Pp open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Univ open Evd diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 01d42fc07..37a05bbe5 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -3,7 +3,7 @@ (*i*) open Names -(*i open Generic i*) +(* open Generic *) open Term open Univ open Evd diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 68cd846b7..e0c951c22 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -5,7 +5,7 @@ open Pp open Util open Names open Univ -(*i open Generic i*) +(* open Generic *) open Term open Reduction open Sign diff --git a/kernel/sign.ml b/kernel/sign.ml index eac5c8cc9..27aa150e6 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -3,7 +3,7 @@ open Names open Util -(*i open Generic i*) +(* open Generic *) open Term (* Signatures *) diff --git a/kernel/sign.mli b/kernel/sign.mli index 889c79b4e..bb2e083de 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -3,7 +3,7 @@ (*i*) open Names -(*i open Generic i*) +(* open Generic *) open Term (*i*) diff --git a/kernel/sosub.ml b/kernel/sosub.ml index 7212216ee..4ea19e821 100644 --- a/kernel/sosub.ml +++ b/kernel/sosub.ml @@ -3,7 +3,7 @@ open Util open Names -(*i open Generic i*) +(* open Generic *) open Term (* (* Given a term with variables in it, and second-order substitution, diff --git a/kernel/term.mli b/kernel/term.mli index e4e0e1df5..fe3996c5c 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -5,7 +5,7 @@ open Util open Pp open Names -(*i open Generic i*) +(* open Generic *) (*i*) (*s The sorts of CCI. *) @@ -76,7 +76,7 @@ and typed_type type flat_arity = (name * constr) list * sorts -(*s Functions about typed_type *) +(*s Functions about [typed_type] *) val make_typed : constr -> sorts -> typed_type val make_typed_lazy : constr -> (constr -> sorts) -> typed_type @@ -358,12 +358,6 @@ val args_of_const : constr -> constr array val destEvar : constr -> int * constr array val num_of_evar : constr -> int -(* -(* Destructs an abstract term *) -val destAbst : constr -> section_path * constr array -val path_of_abst : constr -> section_path -val args_of_abst : constr -> constr array -*) (* Destructs a (co)inductive type *) val destMutInd : constr -> inductive val op_of_mind : constr -> inductive_path diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 37dfccf9e..078b6b96b 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -5,7 +5,7 @@ open Pp open Util open Names open Univ -(*i open Generic i*) +(* open Generic *) open Term open Declarations open Sign diff --git a/library/declare.ml b/library/declare.ml index 9f98f3cb5..5d62f067a 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -4,7 +4,7 @@ open Pp open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Sign open Declarations diff --git a/library/global.ml b/library/global.ml index 741d11e75..e58f1b03b 100644 --- a/library/global.ml +++ b/library/global.ml @@ -2,7 +2,7 @@ (* $Id$ *) open Util -(*i open Generic i*) +(* open Generic *) open Term open Instantiate open Sign diff --git a/library/impargs.ml b/library/impargs.ml index 3af4ecbec..30e4c4e50 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -2,7 +2,7 @@ (* $Id$ *) open Names -(*i open Generic i*) +(* open Generic *) open Term open Reduction open Declarations diff --git a/library/indrec.ml b/library/indrec.ml index ddba73abe..655db9af7 100644 --- a/library/indrec.ml +++ b/library/indrec.ml @@ -4,7 +4,7 @@ open Pp open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Declarations open Inductive diff --git a/library/redinfo.ml b/library/redinfo.ml index 9e5c86a52..6bd08a2ff 100644 --- a/library/redinfo.ml +++ b/library/redinfo.ml @@ -3,7 +3,7 @@ open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Declarations open Reduction diff --git a/parsing/astterm.ml b/parsing/astterm.ml index 72b7e1cf5..1a2cc53ae 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -5,7 +5,7 @@ open Pp open Util open Names open Sign -(*i open Generic i*) +(* open Generic *) open Term open Environ open Evd diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4 index f3aaa4e2a..ed8e9a5bf 100644 --- a/parsing/g_minicoq.ml4 +++ b/parsing/g_minicoq.ml4 @@ -5,7 +5,7 @@ open Pp open Util open Names open Univ -(*i open Generic i*) +(* open Generic *) open Term open Environ diff --git a/parsing/pattern.ml b/parsing/pattern.ml index 17a4535a4..f84a2d929 100644 --- a/parsing/pattern.ml +++ b/parsing/pattern.ml @@ -2,7 +2,7 @@ (* $Id$ *) open Util -(*i open Generic i*) +(* open Generic *) open Names open Term open Reduction diff --git a/parsing/pretty.ml b/parsing/pretty.ml index 123f690a8..d9e22af37 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -4,7 +4,7 @@ open Pp open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Declarations open Inductive diff --git a/parsing/termast.ml b/parsing/termast.ml index 0d04bd2b2..b8a39e37f 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -5,7 +5,7 @@ open Pp open Util open Univ open Names -(*i open Generic i*) +(* open Generic *) open Term open Inductive open Sign diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 54869505e..1e48d3443 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1,7 +1,7 @@ open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Declarations open Inductive diff --git a/pretyping/class.ml b/pretyping/class.ml index 5c56ce9b6..6c0da8c20 100644 --- a/pretyping/class.ml +++ b/pretyping/class.ml @@ -4,7 +4,7 @@ open Util open Pp open Names -(*i open Generic i*) +(* open Generic *) open Term open Inductive open Declarations diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 4e991a5fd..f5af725b2 100755 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -9,7 +9,7 @@ open Environ open Libobject open Declare open Term -(*i open Generic i*) +(* open Generic *) open Rawterm (* usage qque peu general: utilise aussi dans record *) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index d4a7ef4a6..7197110bf 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -1,7 +1,7 @@ (* $Id$ *) open Util -(*i open Generic i*) +(* open Generic *) open Names open Term open Reduction diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index a6d06f3f9..ce72f7e01 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -5,7 +5,7 @@ open Pp open Util open Univ open Names -(*i open Generic i*) +(* open Generic *) open Term open Inductive open Sign diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index f9a3fe69b..4f551f31d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -3,7 +3,7 @@ open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Reduction open Instantiate diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 2d35fb753..e94ac55d3 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -5,7 +5,7 @@ open Util open Pp open Names open Univ -(*i open Generic i*) +(* open Generic *) open Term open Sign open Environ diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 295e081a3..41f1878d6 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -4,7 +4,7 @@ open Pp open Util open Names -(*i open Generic i*) +(* open Generic *) open Sign open Evd open Term diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 10c7cee07..f16f77c63 100755 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -11,7 +11,7 @@ open Library open Classops (* open Pp_control -(*i open Generic i*) +(* open Generic *) open Initial *) diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 0f90afeb5..97c6c5306 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -4,7 +4,7 @@ (*i*) open Names open Term -(*i open Generic i*) +(* open Generic *) open Classops open Libobject open Library diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index bd1b88bea..d6d3395e5 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -5,7 +5,7 @@ open Util open Term open Inductive open Names -(*i open Generic i*) +(* open Generic *) open Reduction open Environ open Typeops diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index dde27dbae..87dca45db 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -4,7 +4,7 @@ open Pp open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Inductive open Environ diff --git a/pretyping/typing.ml b/pretyping/typing.ml index cbe8b3601..99f2f09a8 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -3,7 +3,7 @@ open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Environ open Reduction diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 0cd364b93..efc519051 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -4,7 +4,7 @@ open Pp open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Sign open Instantiate diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 5cb4689ae..3e2d96a95 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -5,7 +5,7 @@ open Pp open Util open Stamps open Names -(*i open Generic i*) +(* open Generic *) open Term open Environ open Evd diff --git a/proofs/logic.ml b/proofs/logic.ml index db9b7c110..e06949be3 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -5,7 +5,7 @@ open Pp open Util open Names open Evd -(*i open Generic i*) +(* open Generic *) open Term open Sign open Environ diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index c660b35ef..62629a65b 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -5,7 +5,7 @@ open Pp open Util open Names open Sign -(*i open Generic i*) +(* open Generic *) open Term open Declarations open Environ diff --git a/proofs/refiner.ml b/proofs/refiner.ml index badf6bc7a..f54a8abb0 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -4,7 +4,7 @@ open Pp open Util open Stamps -(*i open Generic i*) +(* open Generic *) open Term open Sign open Evd diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index b96f17af5..7375947f1 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -3,7 +3,7 @@ open Astterm open Closure -(*i open Generic i*) +(* open Generic *) open Libobject open Pattern open Pp diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index e8d4be64e..ec3776c81 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -4,7 +4,7 @@ open Util open Stamps open Names -(*i open Generic i*) +(* open Generic *) open Sign open Term open Instantiate diff --git a/tactics/auto.ml b/tactics/auto.ml index e5dfff04c..acf0b6cc6 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -4,7 +4,7 @@ open Pp open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Sign open Inductive diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index aeb3f306c..ca1d0831a 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -2,7 +2,7 @@ (* $Id$ *) (*i*) -(*i open Generic i*) +(* open Generic *) open Term open Pattern (*i*) diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index 4190cb17d..7e3ac13b2 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -107,7 +107,7 @@ Qed. open Pp open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Environ open Reduction diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 6eab9ae08..09d8885d8 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -4,7 +4,7 @@ open Pp open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Sign open Reduction diff --git a/tactics/elim.ml b/tactics/elim.ml index 0fbfcae9a..2cfcd8559 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -4,7 +4,7 @@ open Pp open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Reduction open Inductive diff --git a/tactics/equality.ml b/tactics/equality.ml index f32562182..bec81d44a 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -5,7 +5,7 @@ open Pp open Util open Names open Univ -(*i open Generic i*) +(* open Generic *) open Term open Inductive open Environ diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index fd54744fe..cc88fbcd7 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -4,7 +4,7 @@ open Pp open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Reduction open Inductive diff --git a/tactics/inv.ml b/tactics/inv.ml index 82863269b..0a09c441b 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -4,7 +4,7 @@ open Pp open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Global open Sign diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 57baf0b15..c5bf51771 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -4,7 +4,7 @@ open Pp open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Sign open Evd diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml index ae0f5a6c9..d5d657365 100644 --- a/tactics/nbtermdn.ml +++ b/tactics/nbtermdn.ml @@ -3,7 +3,7 @@ open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Libobject open Library diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli index f68fc89e7..4cbf696c4 100644 --- a/tactics/nbtermdn.mli +++ b/tactics/nbtermdn.mli @@ -2,7 +2,7 @@ (* $Id$ *) (*i*) -(*i open Generic i*) +(* open Generic *) open Term open Pattern (*i*) diff --git a/tactics/refine.ml b/tactics/refine.ml index f5a95d59c..08105aa9f 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -42,7 +42,7 @@ open Pp open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Tacmach open Sign diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index b77ac413c..d5ee7f965 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -4,7 +4,7 @@ open Pp open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Sign open Declarations diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 4312071b4..a8693a70b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -6,7 +6,7 @@ open Util open Stamps open Names open Sign -(*i open Generic i*) +(* open Generic *) open Term open Inductive open Reduction diff --git a/tactics/tauto.ml b/tactics/tauto.ml index 416e81cd2..7c00a6b1d 100644 --- a/tactics/tauto.ml +++ b/tactics/tauto.ml @@ -6,7 +6,7 @@ open Pp open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Sign open Environ diff --git a/tactics/termdn.ml b/tactics/termdn.ml index 9cdb34ab2..920e6ba31 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -2,7 +2,7 @@ (* $Id$ *) open Util -(*i open Generic i*) +(* open Generic *) open Names open Term open Pattern diff --git a/tactics/termdn.mli b/tactics/termdn.mli index 107026ef6..02415bc3c 100644 --- a/tactics/termdn.mli +++ b/tactics/termdn.mli @@ -2,7 +2,7 @@ (* $Id$ *) (*i*) -(*i open Generic i*) +(* open Generic *) open Term open Pattern (*i*) diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml index 25c63e536..4f071980e 100644 --- a/tactics/wcclausenv.ml +++ b/tactics/wcclausenv.ml @@ -4,7 +4,7 @@ open Pp open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Sign open Reduction diff --git a/toplevel/command.ml b/toplevel/command.ml index 2a15741bf..e23d3b7f9 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -4,7 +4,7 @@ open Pp open Util open Options -(*i open Generic i*) +(* open Generic *) open Term open Declarations open Inductive diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 987daed1b..9a55f5adf 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -5,7 +5,7 @@ open Pp open Util open Names open Sign -(*i open Generic i*) +(* open Generic *) open Term open Declarations open Inductive diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml index bee6f074a..92fb1bd93 100644 --- a/toplevel/fhimsg.ml +++ b/toplevel/fhimsg.ml @@ -4,7 +4,7 @@ open Pp open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Sign open Environ diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index a6e63497d..cefa4d823 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -5,7 +5,7 @@ open Pp open Util open Options open Names -(*i open Generic i*) +(* open Generic *) open Term open Inductive open Indtypes diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml index ab55fe549..7e2b1f5bd 100644 --- a/toplevel/minicoq.ml +++ b/toplevel/minicoq.ml @@ -4,7 +4,7 @@ open Pp open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Sign open Declarations diff --git a/toplevel/record.ml b/toplevel/record.ml index 30f7dbdee..fbf258652 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -4,7 +4,7 @@ open Pp open Util open Names -(*i open Generic i*) +(* open Generic *) open Term open Declarations open Declare |