aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Collapse)AuthorAge
* Extraction: forbid Prop-polymorphism of inductives when extracting to OcamlGravatar letouzey2011-07-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | A particular case in sort-polymorphism of inductive types allows an informative type (such as prod) to have instances in Prop: (I,I) : True * True : Prop This is due to the fact that prod is a singleton type: indeed (I,I) has no informative content. But this invalidates an important invariant for the correctness of the extraction: inductive constructors stop having always the same sort as their inductive type. Consider for instance: Definition f (X:Type)(x:X*X)(g:X->nat) := g (fst x). Definition test := f _ (I,I) (fun _ => 0). Then the inductive element (I,I) is extracted as a logical part __, but during a strict evaluation (i.e. in Ocaml, not Haskell), this __ will be given to fst, and hence to a match, leading to a nasty result (potentially segfault). Haskell is not affected, since fst is never evaluated. This patch adds a check for this situation during any Ocaml extraction, leading for the moment to a fatal error. Some functions in inductive.ml and retyping.ml now have an extra optional argument ?(polyprop=true) that should stay untouched in regular Coq usage, while type-checking done during extraction will disable this prop-polymorphism. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14256 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modops: the strengthening functions can work without any env argumentGravatar letouzey2011-05-17
| | | | | | | The env was used for a particular case of Cbytegen.compile_constant_body, but we can actually guess that it will answer a particular BCallias con. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14134 85f007b7-540e-0410-9357-904b9bb8a0f7
* Print Module (Type) M now tries to print more detailsGravatar letouzey2011-05-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | "Print Module M" prints now by default both a signature (fields with their types) and a body (fields with their types and transparent bodies). "Print Module Type M" could be used both when M is a module or a module Type, it will only display th signature of M. The earlier minimalist behavior (printing only the field names) could be reactivated by option "Set Short Module Printing". For the moment, the content of internal sub-modules and sub-modtypes are not displayed. Note: this commit is an experiment, many sitations are still unsupported. When such situations are encountered, Print Module will fall back on the earlier minimalist behavior. This might occur in particular in presence of "with" annotations, or in the conjonction of a non-global module (i.e. functor or module type) and internal sub-modules. Side effects of this commit: - a better compare function for global_reference, with no allocations at each comparison - Nametab.the_globrevtab is now searched according to user part only of a kernel_name - The printing of an inductive block is now in Printer, and rely less on the Nametab. Instead, we use identifiers in mind_typename and mind_consnames. Note that Print M.indu will not display anymore the pseudo-code "Inductive M.indu ..." but rather "Inductive indu..." git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14117 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix thumb2-related build errorGravatar glondu2011-04-19
| | | | | | | | Bug-Debian: http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=622882 Signed-off-by: Konstantinos Margaritis <markos@genesi-usa.com> Signed-off-by: Stephane Glondu <steph@glondu.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14027 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
| | | | | | | | | | | This reverts commit 33434695615806a85cec88452c93ea69ffc0e719. Conflicts: kernel/term_typing.ml test-suite/success/polymorphism.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13998 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Remove create_evar_defsGravatar msozeau2011-04-13
| | | | | | - Be careful with consider_remaining_unif_problems: it might instantiate an evar, including the current goal! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13995 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix merge.Gravatar msozeau2011-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13994 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Do not make constants with an assigned type polymorphic (wrong unfoldings).Gravatar msozeau2011-04-13
| | | | | | - Add Set Typeclasses Debug/Depth n options for typeclasses eauto. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13989 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13988 85f007b7-540e-0410-9357-904b9bb8a0f7
* Subtyping: align coqtop behavior concerning opaque csts on coqchk's oneGravatar letouzey2011-04-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | After discussion with Bruno and Hugo, coqtop now accepts that an opaque constant in a module type could be implemented by anything of the right type, even if bodies differ. Said otherwise, with respect to subtyping, an opaque constant behaves just as a parameter. This was already the case in coqchk, and a footnote in documentation is advertising for quite some time that: "Opaque definitions are processed as assumptions." Truly, it might seem awkward that "Definition x:=3" can implement "Lemma x:nat. Proof 2. Qed." but the opacity ensures that nothing can go wrong afterwards, since Coq is forced to ignore that the x in signature has body "2". Similarly, "T with Definition x := c" is now legal when T contains an opaque x, even when this x isn't convertible with c. By avoiding accesses to opaque bodies, we also achieve some speedup (less delayed load of .vo final sections containing opaque terms). Nota: the extraction will have to be adapted, since for the moment it might access the body of opaque constants: the warning emitted when doing that should become an error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13987 85f007b7-540e-0410-9357-904b9bb8a0f7
* Replaced printing number of ill-typed branch by printing name of constructorGravatar herbelin2011-04-08
| | | | | | | when a "match" is kernel-ill-typed (probably rarely visible from end user anyway but useful for debugging) + dead code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13969 85f007b7-540e-0410-9357-904b9bb8a0f7
* A few extra combinators about rel_declaration/named_declaration + a bit of docGravatar herbelin2011-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13959 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The recent experiment with -dont-load-proofs in the stdlib showed that this options isn't fully safe: some axioms were generated (Include ? functor application ? This is still to be fully understood). Instead, I've implemented an idea of Yann: only load opaque proofs when we need them. This is almost as fast as -dont-load-proofs (on the stdlib, we're now 15% faster than before instead of 20% faster with -dont-load-proofs), but fully compatible with Coq standard behavior. Technically, the const_body field of Declarations.constant_body now regroup const_body + const_opaque + const_inline in a ternary type. It is now either: - Undef : an axiom or parameter, with an inline info - Def : a transparent definition, with a constr_substituted - OpaqueDef : an opaque definition, with a lazy constr_substitued Accessing the lazy constr of an OpaqueDef might trigger the read on disk of the final section of a .vo, where opaque proofs are located. Some functions (body_of_constant, is_opaque, constant_has_body) emulate the behavior of the old fields. The rest of Coq (including the checker) has been adapted accordingly, either via direct access to the new const_body or via these new functions. Many places look nicer now (ok, subjective notion). There are now three options: -lazy-load-proofs (default), -force-load-proofs (earlier semantics), -dont-load-proofs. Note that -outputstate now implies -force-load-proofs (otherwise the marshaling fails on some delayed lazy). On the way, I fixed what looked like a bug : a module type (T with Definition x := c) was accepted even when x in T was opaque. I also tried to clarify Subtyping.check_constant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13952 85f007b7-540e-0410-9357-904b9bb8a0f7
* CHANGES: a word about recent changes in coqide, about Ctrl-C in vmGravatar letouzey2011-04-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13948 85f007b7-540e-0410-9357-904b9bb8a0f7
* Checks for signals in VM, allowing it to be interrupted by Ctrl-C (experimental)Gravatar letouzey2011-04-01
| | | | | | | | | | | | | | | | | | We simply reuse the ocaml flag caml_signals_are_pending and the function caml_process_pending_signals, and place a test at some place of the interpreter loop (at a similar location as in ocaml byterun/interp.c). The symbols caml_* we use are not officially made public in *.h installed alongside ocaml, but they seem pretty stable (there since at least ocaml 3.10, independent of arch and of byte/asm), so we access them via "extern". For once, thanks dirty C... In addition to that, when catching a Ctrl-C, we reset the vm via "coq_sp = coq_stack_high" as suggested by Benjamin G. This patch should be quite portable, it might even work in win32. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13947 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative to make unification check types at every instanciation of anGravatar msozeau2011-03-11
| | | | | | | | | | | | | evar, and simultaneously make type inference with universes work better. This only exports more functions from kernel/univ, to be able to work with a set of universe variables during type inference. Universe constraints are gradually added during type checking, adding information necessary e.g. to lower the level of unknown Type variables to Prop or Set. There does not seem to be a disastrous performance hit on the stdlib, but might have one on some contribs (hence the "Tentative"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13905 85f007b7-540e-0410-9357-904b9bb8a0f7
* adding eta in the vmGravatar bgregoir2011-03-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13896 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving printing of module typing errors upwards to himsg.ml so as toGravatar herbelin2011-03-05
| | | | | | be able to call term printers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13886 85f007b7-540e-0410-9357-904b9bb8a0f7
* Starting being more explicit on the reasons why module subtyping fails.Gravatar herbelin2011-03-05
| | | | | | | | | Note: I'm unsure about some subtyping error case apparently involving aliases of inductive types (middle of Subtyping.check_inductive); I bound it to some NotEqualInductiveAliases error, but this has to be checked. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13885 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a "feature" about subtyping records: one was expected not onlyGravatar herbelin2011-03-05
| | | | | | | that the fields had the same names but that the parameters of the record had exactly the same names too. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13879 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mod_subst: improving sharing of subst_mpsGravatar letouzey2011-02-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13854 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some more simplification in Mod_substGravatar letouzey2011-02-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13852 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Use transparency information all the way through unification andGravatar msozeau2011-02-17
| | | | | | | | | | conversion. - Fix trans_fconv* to use evars correctly. - Normalize the goal with respect to evars before rewriting in [rewrite], allowing to see instanciations from other subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13844 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mod_typing: some refactoring (common parts about MSEapply and co)Gravatar letouzey2011-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13838 85f007b7-540e-0410-9357-904b9bb8a0f7
* Safe_typing: some refactoring (avoiding copy-paste of record definitions)Gravatar letouzey2011-02-11
| | | | | | | Many of the record definitions for new safe_environment follow the same pattern, we factorize them in a generic add_field function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13837 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mod_subt: some more refactoring, substitution is also separated in two tablesGravatar letouzey2011-02-11
| | | | | | This way, no more mixing of MBI / MPI. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13836 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mod_subst: split delta_resolver in two tables (mp / kn)Gravatar letouzey2011-02-11
| | | | | | | | | This way, no more absurd mixing of mp/kn and Prefix_equiv/Equiv to consider, and hence no more anomaly or assert false left in Mod_subst. As we say here, "faut pas melanger les torchons et les serviettes" ... With these two specialized tables, efficiency might also be better. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13835 85f007b7-540e-0410-9357-904b9bb8a0f7
* compatibility <3.12 (Map.exists Map.singleton)Gravatar pboutill2011-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13829 85f007b7-540e-0410-9357-904b9bb8a0f7
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As said in CHANGES: << The inlining done during application of functors can now be controlled more precisely. In addition to the "!F G" syntax preventing any inlining, we can now use a priority level to select parameters to inline : "<30>F G" means "only inline in F the parameters whose levels are <= 30". The level of a parameter can be fixed by "Parameter Inline(30) foo". When levels aren't given, the default value is 100. One can also use the flag "Set Inline Level ..." to set a level. >> Nota : the syntax "Parameter Inline(30) foo" is equivalent to "Set Inline Level 30. Parameter Inline foo.", and "Include <30>F G" is equivalent to "Set Inline Level 30. Include F G." For instance, in ZBinary, eq is @Logic.eq and should rather be inlined, while in BigZ, eq is (fun x y => [x]=[y]) and should rather not be inlined. We could achieve this behavior by setting a level such as 30 to the parameter eq, and then tweaking the current level when applying functors. This idea of levels might be too restrictive, we'll see, but at least the implementation of this change was quite simple. There might be situation where parameters cannot be linearly ordered according to their "inlinablility". For these cases, we would need to mention names to inline or not at a functor application, and this is a bit more tricky (and might be a pain to use if there are many names). No documentation for the moment, since this feature is experimental and might still evolve. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13807 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
| | | | | | | | | | | | | | | | According to B. Gregoire, this stuff is obsolete. Fine control on when to launch the VM in conversion problems is now provided by VMcast. We were already almost never boxing definitions anymore in stdlib files. "(Un)Boxed Definition foo" will now trigger a parsing error, same with Fixpoint. The option "(Un)Set Boxed Definitions" aren't there anymore, but tolerated (as no-ops), since unknown options raise a warning instead of an error by default. Some more cleaning could be done in the vm. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Make simpl use the proper constant when folding (mutual) fixpointsGravatar letouzey2011-01-27
| | | | | | | | | | | | | | | | | | | | | | | Before this commit, when simpl was finding the constant name for folding some (mutual) fixpoint, this was done via some repr_con followed by make_con. Problem: this doesn't preserve the canonical part of a Names.constant. For instance the following script was buggish: Module M. Fixpoint foo n := match n with O => O | S n => bar n end with bar n := match n with O => O | S n => foo n end. End M. Module N. Include M. (* foo, bar have here "user name" N but "canonical name" M *) Eval simpl in (fun x => bar (S x)). (* Anomaly: uncaught exception Failure "Cannot print a global reference". *) (* since simpl has produce a different bar with both user and canonical N *) TODO : check all other uses of make_con in the rest of the sources... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13803 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rewrite sort_universes to minimize the number of universesGravatar glondu2011-01-25
| | | | | | | | | | | The whole standard library fits in 3 universes (instead of 22 with the previous algorithm). Very costy, time complexity: O(n^4) (if we assume map operations are done in constant time), with n being the number of universe variables. It takes ~35s for the whole stdlib. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13796 85f007b7-540e-0410-9357-904b9bb8a0f7
* In univ.ml, put universe_level primitives in its their own sub-moduleGravatar glondu2011-01-11
| | | | | | | This is merely refactoring so that UniverseL{Map,Set} constructions appear nicely. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13788 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add "Print Sorted Universes"Gravatar glondu2011-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13786 85f007b7-540e-0410-9357-904b9bb8a0f7
* More coherent comment orderingGravatar glondu2011-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13784 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2454: inversion predicate strategy for inferring the typeGravatar herbelin2010-12-19
| | | | | | | of "match" is not general enough; if there is a non dependent type constraint, we also try w/o inversion predicate in the return clause. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13727 85f007b7-540e-0410-9357-904b9bb8a0f7
* Univ: try to avoid a few lookup in the universe graphGravatar letouzey2010-12-18
| | | | | | | | | | | | | | | | | | | | Sometimes the same (repr g u) was done in different functions after being passed u as argument. We rather try to compute (repr g u) as soon as possible, and then pass it instead of u. Beware of sync issues : if g changes, arcu might become obsolete (cf. setlt, setleq, merge ...) Typical code around occurences of declare_univ was doing up to 3 lookups: - is u in g ? - if not we descend again in g to add it - and then later repr is called on the same u. With my safe_repr, we do one lookup if u is in g, and a lookup and an addition otherwise. Ok, declare_univ was rarely used, but it seems nicer this way. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13726 85f007b7-540e-0410-9357-904b9bb8a0f7
* Univ.constraints made fully abstract instead of being a Set of abstract stuffGravatar letouzey2010-12-18
| | | | | | | | | No need to tell the world about the fact that constraints are implemented via caml's Set. Other modules just need to know about the empty and union functions (and addition functions "enforce_geq" and "enforce_eq" that were already there). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13725 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert last commit 13723 on Univ : minor gains and more complex codeGravatar letouzey2010-12-18
| | | | | | | | | | | | | | | | The gains on contribs are quite small, around 3% max, apart from 3 small contribs where it's about 10% (corresponding to 10s each). With last patch, we add quicker lookup for universes in the graph (up to 5 times less calls to cmp_univ_level on an example), but probably more "administrative" work (i.e. addition of updated paths in the graphs, handling pairs of updated graphs and results in functions, etc), and some sharing might also have been lost since graphs changed more. Anyway, little gain and more complex code, let's remove this patch for now ... until the next attempt to speed-up the universe layer. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13724 85f007b7-540e-0410-9357-904b9bb8a0f7
* Univ: an attempt to lazily compact chains of Equiv in a functionnal wayGravatar letouzey2010-12-17
| | | | | | | | We'll see experimentally if this helps... A few more functions could be adapted (e.g. between), and an occurence of compare just discard the compacted graph (in compare_greater) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13723 85f007b7-540e-0410-9357-904b9bb8a0f7
* Univ: two improvements (speed + space)Gravatar letouzey2010-12-16
| | | | | | | | | | | | | - The "compare" function on universes (the one answering EQ|LT|LE|NLE) was launching "collect" for creating the transitive upward closure of u, and then checking if v is in it. We now proceed more lazily, by stopping creating the transitive closure as soon as v is found. - In univ_entry, the first arg u of Equiv(u,v) is removed. It can indeed be retrieved from the key of the universe graph leading to this Equiv. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13719 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Kernel/Term:Gravatar regisgia2010-12-01
| | | | | | | | | - Fix a bug in [comp_term] (casts were ignored). - Improve the efficiency of hash table lookup. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13662 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Kernel/TermGravatar regisgia2010-12-01
| | | | | | | | Remove an unsound optimization. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13661 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Kernel/TermGravatar regisgia2010-12-01
| | | | | | | | Fix an efficiency bug when hash-consing deep [constr]s. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13660 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes from Gregory Malecha. A typo fixed and a better (located) Gravatar msozeau2010-11-15
| | | | | | | error message in case of unnammed record parameters. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13635 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug 2427Gravatar soubiran2010-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13617 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove suspiciously named "implicit" stuff from TermGravatar glondu2010-11-03
| | | | | | | The lambda_implicit series of functions are used only in Indtypes, so we move them there. In the checker, they are already there... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13615 85f007b7-540e-0410-9357-904b9bb8a0f7
* In Univ, unify order_request and constraint_typeGravatar glondu2010-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13614 85f007b7-540e-0410-9357-904b9bb8a0f7
* More generic Univ.dump_universesGravatar glondu2010-11-02
| | | | | | | | Instead of formatting directly to an output channel, provide an output function that handles formatting and I/O. This allows changing the output format. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13610 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reintroduce kind_of_type (used by Presburger contrib)Gravatar glondu2010-10-05
| | | | | | This partially reverts commit r13467. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13497 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 16:59:01 +0000