Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Commits on Jul 23, 2013
  1. Matthieu Sozeau
Commits on Apr 17, 2013
  1. Matthieu Sozeau
  2. Matthieu Sozeau

    - Fix discharge adding spurious global constraints on polymorphic uni…

    mattam82 authored
    …verse variables
    
    appearing in assumptions.
    - Fixes in inductiveops not taking into account universe polymorphic inductives.
    
    Conflicts:
    	library/declare.ml
    	library/decls.ml
    	library/decls.mli
Commits on Apr 5, 2013
  1. after conflict resolution

    Yves Bertot authored
  2. Matthieu Sozeau

    This commit adds full universe polymorphism to Coq.

    mattam82 authored
    Add [Polymorphic] and [Monomorphic] local flag for definitions as well as
    [Set Universe Polymorphism] global flag to make all following definitions
    polymorphic. Mainly syntax for now.
    
    First part of the big changes to the kernel:
    - Const, Ind, Construct now come with a universe level instance
    - It is used for type inference in the kernel, which now also takes
    a graph as input: actually a set of local universe variables and their
    constraints. Type inference just checks that the constraints are enough
    to satisfy its own rules.
    - Remove polymorphic_arity and _knowing_parameters everywhere: we
    don't need full applications for polymorphism to apply anymore, as
    we generate fresh variables at each constant/inductive/constructor
    application. However knowing_parameters variants might be reinstated
    later for optimization.
    - New structures exported in univ.mli:
      - universe_list for universe level instances
      - universe_context(_set) for the local universe constraints, also
    recording which variables will be local and hence generalized after
    inference if defining a polymorphic ind/constant.
    - this patch makes coq stop compiling at indtypes.ml
    
    Adapt kernel, library, pretyping, tactics and toplevel to universe polymorphism.
    Various degrees of integration, places where I was not sure what to do or
    just postponed bigger reorganizations of the code are marked with FIXMEs.
    Main changes:
    - Kernel now checks constraints and does not infer them anymore.
    - The inference functions produce a context of constraints that were checked
    during inference, useful to do double-checking of the univ. poly. code
    but might be removed later.
    - Constant, Inductive entries now have a universe context (local variables
    and constraints) associated to them.
    - Printing, debugging functions for the new structures are also implemented.
    - Now stopping at Logic.v
    - Lots of new code in kernel/univ.ml that should be reviewed.
    - kernel/indtypes probably does not do what's right when inferring inductive
    type constraints.
    - Adapted evd to use the new universe context structure.
    - Did not deal with unification/evar_conv.
    
    - Add externalisation code for universe level instances.
    - Support for polymorphism in pretyping/command and proofs/proofview etc.
      Needed wrapping of [fresh_.._instance] through the evar_map, which
      contains the local state of universes during type-checking.
    - Correct the inductive scheme generation to support polymorphism as well.
    - Have to review kernel code for correctness, and especially rework the
      computation of universe constraints for inductives.
    Stops somewhat later in Logic.v
    
    - Fix naming of local/toplevel universes to be correctly done at typechecking time:
      local variables have no dirpath.
    - Add code to do substitution of universes in modules, not finished yet.
    - Move fresh_* functions out of kernel, it won't ever build a universe level again!
    - Adapt a lot of new_Type to use the correct dirpath and declare the new types in the evar_map
    so we keep track of them.
    - A bit of code factorization (evd_comb moved, pretype_global).
    
    - Refactor more code
    - Adapt plugins code (sometimes wrong, marked with FIXME)
    - Fix cases generating unneeded universe (not sure it's ok though)
    - Fix scheme generation for good, might have opportunity to cleanup
    the terms later.
    
    Init compiles now (which means rewrite, inversion, elim etc.. work as well).
    - Unsolved issue of pretyping to lower sorts properly (to Prop for example).
      This has to do with the (Retyping.get_type_of) giving algebraic universes that
      would appear on the right of constraints.
      This makes checking for dangling universes at the end of pretyping fail,
      hence the check in kernel/univ was removed. It should come back when we have
      a fix for this.
    - Correctly (?) compute the levels of inductive types.
      Removed old code pertaining to universe polymorphism. Note that we generate
      constraint variables for the conclusion of inductive types invariably.
    - Shrink constraints before going to the kernel, combine substitution of the
      smaller universe set with normalization of evars (maybe not done everywhere,
      only ordinary inductives, definitions and proofs)
    - More API reworks overall. tclPUSHCONTEXT can be used to add fresh universes
      to the proof goal (used in a few places to get the right instance.
    - Quick fix for auto that won't work in the long run. It should always have been
      restricted to take constant references as input, without any loss of generality
      over constrs.
    
    Fix some plugins and insertion of non-polymorphic constants in a module.
    Now stops in relation classes.
    
    Cleanup and move code from kernel to library and from pretyping to library too.
    Now there is a unique universe counter declared in library/universes.ml along
    with all the functions to generate new universes and get fresh constant/inductive
    terms.
    - Various function renamings
    - One important change in kernel/univ.ml: now [sup] can be applied to Prop.
    - Adapt records/classes to universe polymorphism
    - Now stops in EqDepFacts due to imprecise universe polymorphism.
    
    Forgot to git add those files.
    
    interp_constr returns the universe context
    
    The context is then pushed through the environment (or proof goal
    sigma).
    - Fix insertion of constants/inductives in env, pushing constraints to
    the global env for non-polymorphic ones.
    - Add Prop as a universe level to do proper type inference with sorts.
    It is allowed to take [sup] of [Prop] now.
    - New nf_evar based on new Evd.map(_undefined)
    - In proofs/logic.ml: conv_leq_goal might create some constraints that
    are now recorded.
    - Adapt Program code to universes.
    
    Merge with latest trunk + fixes
    
    -Use new constr_of_global from universes
    - fix eqschemes to use polymorphic universes
    - begin fixing cctac but f_equal still fails
    - fix [simpl] and rest of tacred
    - all the eq_constr with mkConst foo should be fixed as well, only
    partially done
    
    - Fix term hashing function to recognize equal terms up to universe instances.
    - Fix congruence closure to equate terms that differ only in universe instances,
    these will be resolved by constraints.
    
    Add a set of undefined universe variables to unification.
    Universe variables can now be declared rigid or flexible (unifiable).
    Flexible variables are resolved at the end of typechecking by instantiating
    them to their glb, adding upper bound constraints associated to them.
    Also:
    - Add polymorphic flag for inductives.
    - Fix cooking partially
    - Fix kernel/univ.ml to do normalization of universe expressions at
    the end of substitution.
    
    Correct classes/structures universe inference
    
    - Required a bit of extension in Univ to handle Max properly (sup u
    (u+1)) was returning (max(u,u+1)) for example.
    - Try a version where substitution of universe expressions for universe
    levels is allowed at the end of unification. By an invariant this
    should only instantiate with max() types that are morally "on the
    right" only.
    This is controlled using a rigidity attribute of universe variables,
    also allowing to properly do unification w.r.t. universes during
    typechecking/inference.
    - Currently fails in Vectors/Fin.v because case compilation generates
    "flexible" universes that actually appear in the term...
    
    Fix unification of universe variables.
    
    - Fix choice of canonical universe in presence of universe constraints,
    and do so by relying on a trichotomy for universe variables: rigid
    (won't be substituted), flexible (might be if not substituted by an
    algebraic) and flexible_alg (always substituted).
    - Fix romega code and a few more plugins, most of the standard library
    goes through now.
    - Had to define some inductives as Polymorphic explicitly to make
    proofs go through, more to come, and definitions should be polymorphic
    too, otherwise inconsistencies appear quickly (two uses of the same
    polymorphic ind through monomorphic functions (like nth on lists of
    Props and nats) will fix the monomorphic function's universe with eq
    constraints that are incompatible).
    - Correct universe polymorphism handling for fixpoint/cofixpoint
    definitions.
    
    - Fix romega to use the right universes for list constructors.
    - Fix internalization/externalization to deal properly with the
    implicit parsing of params.
    - Fix fourier tactic w.r.t. GRefs
    
    - Fix substitution saturation of universes.
    - Fix number syntax plugin.
    - Fix setoid_ring to take its coefficients in a Set rather
    than a Type, avoiding a large number of useless universe constraints.
    
    - Fix minor checker decl
    - Fix btauto w.r.t. GRef
    - Fix proofview to normalize universes in the original types as well.
    - Fix definitions of projections to not take two universes at the same level,
    but at different levels instead, avoiding unnecessary constraints that could
    lower the level of one component depending on the use of the other component.
    
    Fix simpl fst, snd to use @fst @snd as they have maximal implicits now.
    
    - More simpl snd, fst fixes.
    - Try to make the nth theory of lists polymorphic.
    
    Check with Enrico if this change is ok. Case appearing in RingMicromega's call
    to congruence l417, through a call to refine -> the_conv_x_leq.
    
    Compile everything.
    - "Fix" checker by deactivating code related to polymorphism, should
    be updated.
    - Make most of List.v polymorphic to help with following definitions.
    - When starting a lemma, normalize w.r.t. universes, so that the types
    get a fixed universe, not refinable later.
    - In record, don't assign a fully flexible universe variable to the record
    type if it is a definitional typeclass, as translate_constant doesn't expect
    an algebraic universe in the type of a constant. It certainly should though.
    - Fix micromega code.
    
    Fix after rebase.
    
    Update printing functions to print the polymorphic status of definitions
    and their universe context.
    
    Refine printing of universe contexts
    
    - Fix printer for universe constraints
    - Rework normalization of constraints to separate the Union-Find result
      from computation of lubs/glbs.
    
    Keep universe contexts of inductives/constants in entries for correct
    substitution inside modules. Abstract interface to get an instantiation
    of an inductive with its universe substitution in the kernel (no
    substitution if the inductive is not polymorphic, even if mind_universes
    is non-empty).
    
    Make fst and snd polymorphic, fix instances in RelationPairs to use
    different universes for the two elements of a pair.
    
    - Fix bug in nf_constraints: was removing Set <= constraints, but should
    remove Prop <= constraints only.
    - Make proj1_sig, projT1... polymorphic to avoid weird universe unifications,
    giving rise to universe inconsistenties.
    
    Adapt auto hints to polymorphic references.
    
    Really produce polymorphic hints... second try
    
    - Remove algebraic universes that can't appear in the goal when taking the
      type of a lemma to start.
    
    Proper handling of universe contexts in clenv and auto so that
    polymorphic hints are really refreshed at each application.
    
    Fix erroneous shadowing of sigma variable.
    
    - Make apparent the universe context used in pretyping, including information
    about flexibility of universe variables.
    - Fix induction to generate a fresh constant instance with flexible universe variables.
    
    Add function to do conversion w.r.t. an evar map and its local universes.
    
    - Fix define_evar_as_sort to not forget constraints coming from the refinement.
    - Do not nf_constraints while we don't have the whole term at hand to substitute in.
    
    - Move substitution of full universes to Universes
    - Normalize universes inside an evar_map when doing nf_evar_map_universes.
    - Normalize universes at each call to interp_ltac (potentially expensive)
    
    Do not normalize all evars at each call to interp_gen in tactics: rather
    incrementally normalize the terms at hand, supposing the normalization of universes
    will concern only those appearing in it (dangerous but much more efficient).
    
    Do not needlessly generate new universes constraints for projections of records.
    
    Correct polymorphic discharge of section variables.
    
    Fix autorewrite w.r.t. universes: polymorphic rewrite hints get fresh universe
    instances at each application.
    
    Fix r2l rewrite scheme to support universe polymorphism
    
    Fix a bug in l2r_forward scheme and fix congruence scheme to handle polymorphism correctly.
    
    Second try at fixing autorewrite, cannot do without pushing the constraints and the set of fresh
    universe variables into the proof context.
    
    - tclPUSHCONTEXT allow to set the ctx universe variables as flexible or rigid
    - Fix bug in elimschemes, not taking the right sigma
    
    Wrong sigma used in leibniz_rewrite
    
    Avoid recomputation of bounds for equal universes in normalization of constraints,
    only the canonical one need to be computed.
    
    Make coercions work with universe polymorphic projections.
    
    Fix eronneous bound in universes constraint solving.
    
    Make kernel reduction and term comparison strictly aware of universe instances,
    with variants for relaxed comparison that output constraints.
    Otherwise some constraints that should appear during pretyping don't and we generate
    unnecessary constraints/universe variables.
    Have to adapt a few tactics to this new behavior by making them universe aware.
    
    - Fix elimschemes to minimize universe variables
    - Fix coercions to not forget the universe constraints generated by an application
    - Change universe substitutions to maps instead of assoc lists.
    - Fix absurd tactic to handle univs properly
    - Make length and app polymorphic in List, unification sets their levels otherwise.
    
    Move to modules for namespace management instead of long names in universe code.
    
    More putting things into modules.
    
    Change evar_map structure to support an incremental substitution of universes
    (populated from Eq constraints), allowing safe and fast inference of precise levels,
    without computing lubs.
    - Add many printers and reorganize code
    - Extend nf_evar to normalize universe variables according to the substitution.
    - Fix ChoiceFacts.v in Logic, no universe inconsistencies anymore. But Diaconescu
    still has one (something fixes a universe to Set).
    - Adapt omega, functional induction to the changes.
    
    Fix congruence, eq_constr implem, discharge of polymorphic inductives.
    
    Fix merge in auto.
    
    The [-parameters-matter] option (formerly relevant_equality).
    
    Add -parameters-matter to coqc
    
    Do compute the param levels at elaboration time if parameters_matter.
    
    - Fix generalize tactic
    - add ppuniverse_subst
    - Start fixing normalize_universe_context w.r.t. normalize_univ_variables.
    
    - Fix HUGE bug in Ltac interpretation not folding the sigma correctly if interpreting a tactic application
    to multiple arguments.
    - Fix bug in union of universe substitution.
    
    - rename parameters-matter to indices-matter
    - Fix computation of levels from indices not parameters.
    
    - Fixing parsing so that [Polymorphic] can be applied to gallina extensions.
    - When elaborating definitions, make the universes from the type rigid when
    checking the term: they should stay abstracted.
    - Fix typeclasses eauto's handling of universes for exact hints.
    
    Rework all the code for infering the levels of inductives and checking their
    allowed eliminations sorts.
    
    This is based on the computation of a natural level for an inductive type I.
    The natural level [nat] of [I : args -> sort := c1 : A1 -> I t1 .. cn : An -> I tn] is
    computed by taking the max of the levels of the args (if indices matter) and the
    levels of the constructor arguments.
    The declared level [decl] of I is [sort], which might be Prop, Set or some Type u (u fresh
    or not).
    If [decl >= nat && not (decl = Prop && n >= 2)], the level of the inductive is [decl],
    otherwise, _smashing_ occured.
    If [decl] is impredicative (Prop or Set when Set is impredicative), we accept the
    declared level, otherwise it's an error.
    
    To compute the allowed elimination sorts, we have the following situations:
    - No smashing occured: all sorts are allowed. (Recall props that are not
    smashed are Empty/Unitary props)
    - Some smashing occured:
     - if [decl] is Type, we allow all eliminations (above or below [decl],
       not sure why this is justified in general).
     - if [decl] is Set, we used smashing for impredicativity, so only
       small sorts are allowed (Prop, Set).
     - if [decl] is Prop, only logical sorts are allowed: I has either
       large universes inside it or more than 1 constructor.
       This does not treat the case where only a Set appeared in I which
       was previously accepted it seems.
    
    All the standard library works with these changes. Still have to cleanup
    kernel/indtypes.ml. It is a good time to have a whiskey with OJ.
    
    Thanks to Peter Lumsdaine for bug reporting:
    - fix externalisation of universe instances (still appearing when no Printing Universes)
    - add [convert] and [convert_leq] tactics that keep track of evars and universe constraints.
    - use them in [exact_check].
    
    Fix odd behavior in inductive type declarations allowing to silently lower a Type i parameter
    to Set for squashing a naturally Type i inductive to Set. Reinstate the LargeNonPropInductiveNotInType
    exception.
    
    Fix the is_small function not dealing properly with aliases of Prop/Set in Type.
    
    Add check_leq in Evd and use it to decide if we're trying to squash an
    inductive naturally in some Type to Set.
    
    - Fix handling of universe polymorphism in typeclasses Class/Instance declarations.
    - Don't allow lowering a rigid Type universe to Set silently.
    
    - Move Ring/Field back to Type. It was silently putting R in Set due to the definition of ring_morph.
    - Rework inference of universe levels for inductive definitions.
    - Make fold_left/right polymorphic on both levels A and B (the list's type). They don't have to be
    at the same level.
    
    Handle selective Polymorphic/Monomorphic flag right for records.
    
    Remove leftover command
    
    Fix after update with latest trunk.
    
    Backport patches on HoTT/coq to rebased version of universe polymorphism.
    
    - Fix autorewrite wrong handling of universe-polymorphic rewrite rules. Fixes part of issue #7.
    - Fix the [eq_constr_univs] and add an [leq_constr_univs] to avoid eager equation of universe
     levels that could just be inequal. Use it during kernel conversion. Fixes issue #6.
    - Fix a bug in unification that was failing too early if a choice in unification of universes
     raised an inconsistency.
    - While normalizing universes, remove Prop in the le part of Max expressions.
    - Stop rigidifying the universes on the right hand side of a : in definitions.
    - Now Hints can be declared polymorphic or not. In the first case they
     must be "refreshed" (undefined universes are renamed) at each application.
    - Have to refresh the set of universe variables associated to a hint
     when it can be used multiple times in a single proof to avoid fixing
     a level... A better & less expensive solution should exist.
    - Do not include the levels of let-ins as part of records levels.
    - Fix a NotConvertible uncaught exception to raise a more informative
     error message.
    - Better substitution of algebraics in algebraics (for universe variables that
     can be algebraics).
    - Fix issue #2, Context was not properly normalizing the universe context.
    - Fix issue with typeclasses that were not catching UniverseInconsistencies
      raised by unification, resulting in early failure of proof-search.
    - Let the result type of definitional classes be an algebraic.
    - Adapt coercions to universe polymorphic flag (Identity Coercion etc..)
    - Move away a dangerous call in autoinstance that added constraints for every
    polymorphic definitions once in the environment for no use.
    
    Forgot one part of the last patch on coercions.
    
    - Adapt auto/eauto to polymorphic hints as well.
    - Factor out the function to refresh a clenv w.r.t. undefined universes.
    
    Use leq_univ_poly in evarconv to avoid fixing universes.
    
    Disallow polymorphic hints based on a constr as it is not possible to infer their universe
    context. Only global references can be made polymorphic. Fixes issue #8.
    
    Fix SearchAbout bug (issue #10).
    
    Fix program w.r.t. universes: the universe context of a definition changes
    according to the successive refinements due to typechecking obligations.
    This requires the Proof modules to return the generated universe substitution
    when finishing a proof, and this information is passed in the closing hook.
    The interface is not very clean, will certainly change in the future.
    
    - Better treatment of polymorphic hints in auto: terms can be polymorphic now, we refresh their
    context as well.
    - Needs a little change in test-pattern that seems breaks multiary uses of destruct in NZDiv.v, l495.
    FIX to do.
    
    Fix [make_pattern_test] to keep the universe information around and still
    allow tactics to take multiple patterns at once.
    
    - Fix printing of universe instances that should not be factorized blindly
    - Fix handling of the universe context in program definitions by allowing the
    hook at the end of an interactive proof to give back the refined universe context,
    before it is transformed in the kernel.
    - Fix a bug in evarconv where solve_evar_evar was not checking types of instances,
    resulting in a loss of constraints in unification of universes and a growing number
    of useless parametric universes.
    
    - Move from universe_level_subst to universe_subst everywhere.
    
    - Changed representation of universes for a canonical one
    - Adapt the code so that universe variables might be substituted by
    arbitrary universes (including algebraics). Not used yet except for
    polymorphic universe variables instances.
    
    - Adapt code to new constraint structure.
    - Fix setoid rewrite handling of evars that was forgetting the initial
    universe substitution !
    - Fix code that was just testing conversion instead of keeping the
    resulting universe constraints around in the proof engine.
    - Make a version of reduction/fconv that deals with the more general
    set of universe constraints.
    
    - [auto using] should use polymorphic versions of the constants.
    - When starting a proof, don't forget about the algebraic universes in
    the universe context.
    
    Rationalize substitution and normalization functions for universes.
    Also change back the structure of universes to avoid considering levels
    n+k as pure levels: they are universe expressions like max.
    Everything is factored out in the Universes and Univ modules now and
    the normalization functions can be efficient in the sense that they
    can cache the normalized universes incrementally.
    
    - Adapt normalize_context code to new normalization/substitution functions.
    - Set more things to be polymorphic, e.g. in Ring or SetoidList for the rest
    of the code to work properly while the constraint generation code is not adapted.
    And temporarily extend the universe constraint code in univ to solve max(is) = max(js)
    by first-order unification (these constraints should actually be implied not enforced).
    - Fix romega plugin to use the right universes for polymorphic lists.
    - Fix auto not refreshing the poly hints correctly.
    
    - Proper postponing of universe constraints during unification, avoid making
    arbitrary choices.
    - Fix nf_evars_and* to keep the substitution around for later normalizations.
    - Do add simplified universe constraints coming from unification during typechecking.
    - Fix solve_by_tac in obligations to handle universes right, and the corresponding
    substitution function.
    
    Test global universe equality early during simplication of constraints.
    
    Better hashconsing, but still not good on universe lists.
    
    - Add postponing of "lub" constraints that should not be checked early,
    they are implied by the others.
    - Fix constructor tactic to use a fresh constructor instance avoiding
    fixing universes.
    - Use [eq_constr_universes] instead of [eq_constr_univs] everywhere,
    this is the comparison function that doesn't care about the universe
    instances.
    - Almost all the library compiles in this new setting, but some more tactics
    need to be adapted.
    
    - Reinstate hconsing.
    - Keep Prop <= u constraints that can be used to set the level of a universe
    metavariable.
    
    Add better hashconsing and unionfind in normalisation of constraints.
    Fix a few problems in choose_canonical, normalization and substitution functions.
    
    Fix after merge
    
    Fixes after rebase with latest Coq trunk, everything compiles again,
    albeit slowly in some cases.
    - Fix module substitution and comparison of table keys in conversion
    using the wrong order (should always be UserOrd now)
    - Cleanup in universes, removing commented code.
    - Fix normalization of universe context which was assigning global
    levels to local ones. Should always be the other way!
    - Fix universe implementation to implement sorted cons of universes
    preserving order. Makes Univ.sup correct again, keeping universe in
    normalized form.
    - In evarconv.ml, allow again a Fix to appear as head of a weak-head normal
    form (due to partially applied fixpoints).
    - Catch anomalies of conversion as errors in reductionops.ml, sad but
    necessary as eta-expansion might build ill-typed stacks like FProd,
    [shift;app Rel 1], as it expands not only if the other side is rigid.
    - Fix module substitution bug in auto.ml
    
    - Fix case compilation: impossible cases compilation was generating useless universe
    levels. Use an IDProp constant instead of the polymorphic identity to not influence
    the level of the original type when building the case construct for the return type.
    - Simplify normalization of universe constraints.
    - Compute constructor levels of records correctly.
    
    Fall back to levels for universe instances, avoiding issues of unification.
    Add more to the test-suite for universe polymorphism.
    
    Fix after rebase with trunk
    
    Fix substitution of universes inside fields/params of records to be made
    after all normalization is done and the level of the record has been
    computed.
    
    Proper sharing of lower bounds with fixed universes.
    
    Conflicts:
    	library/universes.ml
    	library/universes.mli
    
    Constraints were not enforced in compilation of cases
    
    Fix after rebase with trunk
    
    - Canonical projections up to universes
    - Fix computation of class/record universe levels to allow
    squashing to Prop/Set in impredicative set mode.
    
    - Fix descend_in_conjunctions to properly instantiate projections with universes
    - Avoid Context-bound variables taking extra universes in their associated universe context.
    
    - Fix evar_define using the wrong direction when refreshing a universe under cumulativity
    - Do not instantiate a local universe with some lower bound to a global one just because
    they have the same local glb (they might not have the same one globally).
    
    - Was loosing some global constraints during normalization (brought again by the kernel), fixed now.
    - Proper [abstract] with polymorphic lemmas (polymorphic if the current proof is).
    - Fix silly bug in autorewrite: any hint after the first one was always monomorphic.
    
    - Fix fourier after rebase
    - Refresh universes when checking types of metas in unification (avoid (sup (sup univ))).
    - Speedup a script in FSetPositive.v
    
    Rework definitions in RelationClasses and Morphisms to share universe
    levels as much as possible. This factorizes many useless x <=
    RelationClasses.foo constraints in code that uses setoid rewriting.
    Slight incompatible change in the implicits for Reflexivity and
    Irreflexivity as well.
    
    - Share even more universes in Morphisms using a let.
    - Use splay_prod instead of splay_prod_assum which doesn't reduce let's
    to find a relation in setoid_rewrite
    - Fix [Declare Instance] not properly dealing with let's in typeclass contexts.
    
    Fixes in inductiveops, evarutil.
    
    Patch by Yves Bertot to allow naming universes in inductive definitions.
    
    Fixes in tacinterp not propagating evars correctly.
    
    Fix for issue #27: lowering a Type to Prop is allowed during
    inference (resulting in a Type (* Set *)) but kernel reduction
    was wrongly refusing the equation [Type (*Set*) = Set].
Commits on Apr 2, 2013
  1. Revised infrastructure for lazy loading of opaque proofs

    letouzey authored
     Get rid of the LightenLibrary hack : no more last-minute
     collect of opaque terms and Obj.magic tricks. Instead, we
     make coqc accumulate the opaque terms as soon as constant_bodies
     are created outside sections. In these cases, the opaque
     terms are placed in a special table, and some (DirPath.t * int)
     are used as indexes in constant_body. In an interactive session,
     the local opaque terms stay directly stored in the constant_body.
    
     The structure of .vo file stays similar : magic number, regular
     library structure, digest of the first part, array of opaque terms.
     In addition, we now have a final checksum for checking the
     integrity of the whole .vo file. The other difference is that
     lazy_constr aren't changed into int indexes in .vo files, but are
     now coded as (substitution list * DirPath.t * int). In particular
     this approach allows to refer to opaque terms from another
     library. This (and accumulating substitutions in lazy_constr)
     seems to greatly help decreasing the size of opaque tables :
     -20% of vo size on the standard library :-). The compilation times
     are slightly better, but that can be statistic noise.
    
     The -force-load-proofs isn't active anymore : it behaves now
     just like -lazy-load-proofs. The -dont-load-proofs mode has
     slightly changed : opaque terms aren't seen as axioms anymore,
     but accessing their bodies will raise an error.
    
     Btw, API change : Declareops.body_of_constant now produces directly
     a constr option instead of a constr_substituted option
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16382 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Mar 28, 2013
  1. Safe_typing+Libary: use some arrays instead of lists in vo structures

    letouzey authored
     Very little space saved this way, but it would hurt either...
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16375 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Mar 26, 2013
  1. Pierre-Marie Pédrot

    Synchronizing loadpath with the backtrack mechanism.

    ppedrot authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16373 85f007b7-540e-0410-9357-904b9bb8a0f7
  2. Pierre-Marie Pédrot

    Moved the Loadpath part of Library to its own file, and documented

    ppedrot authored
    the interface.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16372 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Mar 23, 2013
  1. Pierre-Marie Pédrot

    Minor code cleaning in CArray / CList.

    ppedrot authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16351 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Mar 21, 2013
  1. Pierre-Marie Pédrot

    Removing mandatory suffixes for library files.

    ppedrot authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16332 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Mar 13, 2013
  1. Modules and ppvernac, sequel of Enrico's commit 16261

    letouzey authored
     After some investigation, I see no reason to try to hack
     the nametab in ppvernac, since everything happens there
     at a lower level (constr_expr). So the offending code that
     Enrico protected with a State.with_state_protection is now gone.
    
     By the way, moved some types from Declaremods to Vernacexpr
     to avoid some dependencies
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16300 85f007b7-540e-0410-9357-904b9bb8a0f7
  2. Declaremods: a few syntactic improvements

    letouzey authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16299 85f007b7-540e-0410-9357-904b9bb8a0f7
  3. Restrict (try...with...) to avoid catching critical exn (part 8)

    letouzey authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16284 85f007b7-540e-0410-9357-904b9bb8a0f7
  4. Restrict (try...with...) to avoid catching critical exn (part 6)

    letouzey authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16282 85f007b7-540e-0410-9357-904b9bb8a0f7
  5. Restrict (try...with...) to avoid catching critical exn (part 5)

    letouzey authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16281 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Mar 12, 2013
  1. Restrict (try...with...) to avoid catching critical exn (part 1)

    letouzey authored
     Why? : avoid catching (and probably ignoring) exceptions
     such as Sys.Break, anomalies, assertions, leading to undetected
     bugs and ignored Ctrl-C.
    
     How? : when the precise exception(s) concerned by the try is
     known, use them explicitely in the "with". Otherwise, let's use
     the pattern "with e when Errors.noncritical e -> "
    
     Particular case : when an exception is catched and reraised
     immediately after some adjustments, we leave it untouched.
     Simply, for easily identifying these situations later, the name
     of the exception variable is changed to "reraise".
    
     Please also adopt this coding style. Automatic checks based
     on the "mascot" tool of X. Clerc will be runned regularly.
     If you want to avoid to check a particular try...with, use
     the variable name "any" after the "with".
    
     All these changes have been tested using the standard library
     and the test-suite, but unfortunately this is far from ensuring
     that coqtop behaves as before. We'll see after the nightly bench...
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16276 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Mar 11, 2013
  1. Pierre-Marie Pédrot

    Added a Local Definition vernacular command. This type of definition

    ppedrot authored
    has to be refered through its qualified name even when the module
    containing it is imported.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16263 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Mar 2, 2013
  1. A quick and dirty approach to private inductive types

    Yves Bertot authored
    Types for which computable functions are provided, but pattern-matching is disallowed.
    This kind of type can be used to simulate simple forms of higher inductive types, with
    convertibility for applications of the inductive principle to 0-constructors
Commits on Feb 26, 2013
  1. kernel/declarations becomes a pure mli

    letouzey authored
     - constr_substituted and lazy_constr are now in a dedicated kernel/lazyconstr.ml
     - the functions that were in declarations.ml (mostly substitution utilities
       and hashcons) are now in kernel/declareops.ml
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16250 85f007b7-540e-0410-9357-904b9bb8a0f7
  2. Names: shortcuts for building {kn, constant, mind} with empty sections

    letouzey authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16249 85f007b7-540e-0410-9357-904b9bb8a0f7
  3. Mod_subst: misc reformulations

    letouzey authored
     * Remove the mind_of_delta and constant_of_delta functions,
       prefer instead the {mind,constant}_of_delta_kn functions.
    
     * Attempt to make subst_ind and subst_con0 more self-contained
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16247 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Feb 24, 2013
  1. Reduced the noise level when dynlinking in bytecode mode or when

    mdenes authored
    -no-native-compiler flag is on.
    
    
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16239 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Feb 19, 2013
  1. avoid (Int.equal (cmp ...) 0) when a boolean equality exists

    letouzey authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16222 85f007b7-540e-0410-9357-904b9bb8a0f7
  2. Dir_path --> DirPath

    letouzey authored
     Ok, this is merely a matter of taste, but up to now the usage
     in Coq is rather to use capital letters instead of _ in the
     names of inner modules.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7
  3. module_path --> ModPath.t, kernel_name --> KerName.t

    letouzey authored
    For the moment, the compatibility names about these new modules
    are still used in the rest of Coq.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16220 85f007b7-540e-0410-9357-904b9bb8a0f7
  4. Classops : avoid some use of Gmap

    letouzey authored
     Gmap uses Pervasives.compare which may interact badly with
     structures like pairs of kernel names
    
     For the moment, we consider elements in classes and coercions only
     according to their user kernel name: this provides maximal compatibility.
     But it could be interesting to try using comparision according to
     canonical kernel names...
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16218 85f007b7-540e-0410-9357-904b9bb8a0f7
  5. Names: revised representation of constants and mutual_inductive

    letouzey authored
     - a module KernelPair for improving sharing between constant and mind
     - shorter representation than a pair when possible
     - exports comparisions on constant and mind and ...
     - a kn_equal function instead of Int.equal (kn_ord ...) 0
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16217 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Feb 18, 2013
  1. use List.rev_map whenever possible

    letouzey authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16211 85f007b7-540e-0410-9357-904b9bb8a0f7
  2. Minor code cleanups, especially take advantage of Dir_path.is_empty

    letouzey authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16210 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Feb 1, 2013
  1. v8.4: Granting bug/wish #2976 (turning anomaly on input_value into ni…

    herbelin authored
    …ce message)
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16183 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Jan 28, 2013
  1. Fixed bug #2966 (de Bruijn error in computation of heads for coercions).

    herbelin authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16168 85f007b7-540e-0410-9357-904b9bb8a0f7
  2. Pierre-Marie Pédrot

    Actually adding backtrace handling.

    ppedrot authored
    I hope I did not forget some [with] clauses. Otherwise, some
    stack frame will be missing from the debug.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16167 85f007b7-540e-0410-9357-904b9bb8a0f7
  3. Pierre-Marie Pédrot

    Uniformization of the "anomaly" command.

    ppedrot authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Jan 27, 2013
  1. Improving formatting of output of "Test table".

    herbelin authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16159 85f007b7-540e-0410-9357-904b9bb8a0f7
Something went wrong with that request. Please try again.