aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Collapse)AuthorAge
* Modulification of identifierGravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved Intset and Intmap to Int namespace.Gravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16067 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renamed Option.Misc.compare to the more uniform Option.equal.Gravatar ppedrot2012-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16063 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finish patch for Hint Resolve, stopping to generate new constant names forGravatar msozeau2012-12-08
| | | | | | | hints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16052 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evarconv: Fix #2936 + commentsGravatar pboutill2012-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16011 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reductionops uses Closure.redsGravatar pboutill2012-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16009 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed some FIXME related to equality on universes.Gravatar ppedrot2012-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16007 85f007b7-540e-0410-9357-904b9bb8a0f7
* Small cleaning of interface in UnivGravatar ppedrot2012-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16006 85f007b7-540e-0410-9357-904b9bb8a0f7
* More equality functionsGravatar ppedrot2012-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15998 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug #2930: folded let-in's were hiding a violation to the occurGravatar herbelin2012-11-25
| | | | | | | | | | | | check condition in pattern-unification, resulting in the instantiation of evars by terms depending on themselves, henceforth leading eventually to a stack overflow. Occur-check in the arguments of evars was also missing. [Also fixed what looked like a typo in the env passed to project_evar_on_evar on line 1611.] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15996 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a constr_pattern_eqGravatar ppedrot2012-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15995 85f007b7-540e-0410-9357-904b9bb8a0f7
* Monomorphization (pretyping)Gravatar ppedrot2012-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15994 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning and small optimization in CList.Gravatar ppedrot2012-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15988 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a CString module.Gravatar ppedrot2012-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15968 85f007b7-540e-0410-9357-904b9bb8a0f7
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
| | | | | | | | | | | | | | | | | the new Int module. Only the most obvious were removed, so there are a lot more in the wild. This may sound heavyweight, but it has two advantages: 1. Monomorphization is explicit, hence we do not miss particular optimizations of equality when doing it carelessly with the generic equality. 2. When we have removed all the generic equalities on integers, we will be able to write something like "let (=) = ()" to retrieve all its other uses (mostly faulty) spread throughout the code, statically. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15957 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing another bunch of generic equalitiesGravatar ppedrot2012-11-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15955 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reversed roles of undefined/defined evars in Evd, thus saving preciousGravatar ppedrot2012-11-03
| | | | | | | time when requesting only undefined evars (which is actually most often the case, as in Goal.advance). Hopefully this should not disrupt anything. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15952 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed many calls to OCaml generic equality. This was done byGravatar ppedrot2012-10-29
| | | | | | | | writing our own comparison functions, and enforcing monomorphization in many places. This should be more efficient, btw. Still a work in progress. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15932 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
| | | | | | | | | | | | | instead of a general constr: this is the most common case and does not loose generality (one can simply define constrs before Hint Resolving them). Benefits: - Natural semantics for typeclasses, not class resolution needed at Hint Resolve time, meaning less trouble for users as well. - Ability to [Hint Remove] any hint so declared. - Simplifies the implementation as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15930 85f007b7-540e-0410-9357-904b9bb8a0f7
* univ inconsistency error message gives evidence of a cycleGravatar barras2012-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15898 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adapt pieces of code needing -rectypesGravatar letouzey2012-10-06
| | | | | | | | | | | | * in Matching and Tacinterp : ad-hoc types for encoding matching result and "next" continuation * in Class_tactics, occurrences of types such as "type t = (foo * (unit->t) option" have been specialized to something like type t = TNone | TSome of foo * (unit -> t) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15869 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improving error message when abtraction over goal (abstract_list_allGravatar herbelin2012-10-04
| | | | | | | used when applying schemes - induction, rewrite, ...) is well-typed but not of the right type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15853 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
* More cleaning in CArray...Gravatar ppedrot2012-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15819 85f007b7-540e-0410-9357-904b9bb8a0f7
* More cleanup of Util: utf8 aspects moved to a new file unicode.mlGravatar letouzey2012-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15818 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning interface of Util.Gravatar ppedrot2012-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15817 85f007b7-540e-0410-9357-904b9bb8a0f7
* More cleaning on Utils and CList. Some parts of the code beingGravatar ppedrot2012-09-17
| | | | | | peculiarly messy, I hope I did not introduce too many bugs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15815 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some documentation and cleaning of CList and Util interfaces.Gravatar ppedrot2012-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15805 85f007b7-540e-0410-9357-904b9bb8a0f7
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
| | | | | | Util module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15802 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
| | | | | | | | | List module. That way, an "open Util" in the header permits using any function of CList in the List namespace (and in particular, this permits optimized reimplementations of the List functions, as, for example, tail-rec implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
| | | | | | | | | | compiler warnings). I was afraid that such a brutal refactoring breaks some obscure invariant about linking order and side-effects but the standard library still compiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | especially about unused definitions, unused opens and unused rec flags. The following patch uses information gathered using these warnings to clean Coq source tree. In this patch, I focused on warnings whose fix are very unlikely to introduce bugs. (a) "unused rec flags". They cannot change the semantics of the program but only allow the inliner to do a better job. (b) "unused type definitions". I only removed type definitions that were given to functors that do not require them. Some type definitions were used as documentation to obtain better error messages, but were not ascribed to any definition. I superficially mentioned them in one arbitrary chosen definition to remove the warning. This is unaesthetic but I did not find a better way. (c) "unused for loop index". The following idiom of imperative programming is used at several places: "for i = 1 to n do that_side_effect () done". I replaced "i" with "_i" to remove the warning... but, there is a combinator named "Util.repeat" that would only cost us a function call while improving readibility. Should'nt we use it? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15797 85f007b7-540e-0410-9357-904b9bb8a0f7
* correct some ends of .mllib files (avoid a broken tolink.ml)Gravatar letouzey2012-08-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15766 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unification in Evar_conv uses an abstract machine stateGravatar pboutill2012-08-09
| | | | | | | | | It uses a term in front of a stack instead of a term in front of a list of applied terms. From outside of eq_appr_x nothing should have changed. Nasty evar instantiation bug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15719 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid Pp.std_ppcmds in Misctypes.sort_infoGravatar letouzey2012-08-07
| | | | | | | | Otherwise, after a Set Printing Universes we may end on a comparison of Pp.std_ppcmds, which may fail on functional values (cf. Constrextern.check_same_type), as notice by Pierre-Marie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15697 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing #2836 (materialize_evar might refine as a side effect theGravatar herbelin2012-07-29
| | | | | | | | | | | current evar to project; this may happen if this evar is dependent and is involved in evar-evar conversion problem eventually solved by instantiating the current evar; could maybe be optimized when the evar to materialize has invertible instance in which case define_evar_from_virtual_equation applied on the current evar could be shortcut, avoiding to create an evar). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15657 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix eta contraction in ReductionopsGravatar pboutill2012-07-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15650 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reductionops refactoringGravatar pboutill2012-07-20
| | | | | | | | | | | Semantic changes are : - whd_nored_stack remplaces a defined meta by its value whereas the old whd_stack didn't. - Zcase and Zfix are alwais put on stack. iota_flag is checked by constructors and cofix. - simpl uses its own whd_ function that do not touch at matched term git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15634 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing test-suiteGravatar pboutill2012-07-20
| | | | | | | | - bug in r15614: hnf was identity - fix Print Assumptions - bug in r15624: Dump glob of Print About only for Glob git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15630 85f007b7-540e-0410-9357-904b9bb8a0f7
* flex_maybeflex factoringGravatar pboutill2012-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15618 85f007b7-540e-0410-9357-904b9bb8a0f7
* miller_pfenning unification code factoringGravatar pboutill2012-07-12
| | | | | | Mind that the behavior of MaybeFlexible, Flexible changes \! (we solve_pattern_eqn using the new list and not the old one) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15617 85f007b7-540e-0410-9357-904b9bb8a0f7
* flex_kind_of_term does not have a copy of termGravatar pboutill2012-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15616 85f007b7-540e-0410-9357-904b9bb8a0f7
* evar reduction is already made by whd_*Gravatar pboutill2012-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15615 85f007b7-540e-0410-9357-904b9bb8a0f7
* tacred uses stack_reduction_function instead of state_reduction_functionGravatar pboutill2012-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15614 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix regression introduced in r15418 that broke MathClasses. In program mode, ↵Gravatar msozeau2012-07-11
| | | | | | | | | try program coercions before the last resort typeclass resolution to resolve a conversion problem. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15595 85f007b7-540e-0410-9357-904b9bb8a0f7
* Another correction to the dependent existential variable printingGravatar aspiwack2012-07-10
| | | | | | | | for emacs mode. Hopefully fixes Bug 2678 this time. Much saner and more compact code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15573 85f007b7-540e-0410-9357-904b9bb8a0f7
* Continuing r15459: it helps testing occur-check early in someGravatar herbelin2012-07-06
| | | | | | | | | situations (see rewrite MonoidMonadTrans.bind_toLower' in Misc/QuicksortComplexity/monoid_expec.v). Also fixing badly designed test 2817.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15543 85f007b7-540e-0410-9357-904b9bb8a0f7
* Practical fix for bug #1206 (anomaly raised in pretyping instead ofGravatar herbelin2012-07-06
| | | | | | | | | | | error when called on ill-typed term, because pretyping called retyping which in turn is expected to be called only with typable arguments). Incidentally, #1206 shows once more time the problem of confusion between section variables (which morally don't have to be cleared) and their copy in goal (which can be cleared). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15533 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 18:06:57 +0000