| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-04-09 | Readback for int31 values from native compiler. | Maxime Dénès | |
| 2014-04-05 | Fixing bug #3228 (fixing precedence of ltac variables over variables in env). | Hugo Herbelin | |
| 2014-04-04 | Fixing #3262 which revealed a non-progressing, hence looping, | Hugo Herbelin | |
| refinement of evars (in filter_candidates). Incidentally introduced a copy of type "option", "update", which highlights the specific intention of "updating" or not. | |||
| 2014-04-01 | Propagating conversion_problem towards (postponed) evar/evar problems. | Hugo Herbelin | |
| Incidentally simplifies where evar/evar problems are treated (in evar_define and imitate rather than solve_simple_eqn). | |||
| 2014-04-01 | Fixing bug #2900 (evar/evar unif was supposed to be treated in | Hugo Herbelin | |
| solve_simple_eqn but in case the second evar was hidden behind a local variable, it arrived in evar_define and imitate, wrongly assuming progress). | |||
| 2014-03-17 | Evarconv: exact_ise_stack looks to stack head before bodies or branches | Pierre Boutillier | |
| the order of the inspection is a "random" choise but going back to the old behavior makes the compilation of ssreflect/rat.v 5 times faster ... | |||
| 2014-03-16 | consider_remaining_unif_problems respects Conv_oracle | Pierre Boutillier | |
| 2014-03-14 | Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it had | Pierre-Marie Pédrot | |
| no particular purpose. | |||
| 2014-03-10 | Evarconv unification respects Conv_oracle | Pierre Boutillier | |
| 2014-03-10 | MaybeFlexible semantic changes | Pierre Boutillier | |
| From Maybe reducible to Maybe to reduce (but for sure reducible) | |||
| 2014-03-05 | Remove some dead-code (thanks to ocaml warnings) | Pierre Letouzey | |
| The removed code isn't used locally and isn't exported in the signature | |||
| 2014-03-05 | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey | |
| With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment. | |||
| 2014-03-03 | Goptions do not rely anymore on generic equality. | Pierre-Marie Pédrot | |
| 2014-03-02 | Matching --> ConstrMatching (was clashing with OCaml's compiler-libs) | Pierre Letouzey | |
| There are currently two other clashs : Lexer and Errors, but for the moment these ones haven't impacted my experiments with extraction and compiler-libs, while this Matching issue had. And anyway the new name is more descriptive, in the spirit of the recent TacticMatching. | |||
| 2014-03-02 | Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code | Pierre Letouzey | |
| NB: new file miscprint.ml deserves to be part of printing.cma, but should be part of proofs.cma for the moment, due to use in logic.ml | |||
| 2014-03-02 | Adding an equality function over glob_constr | Pierre-Marie Pédrot | |
| 2014-03-01 | Fixing pervasive comparisons | Pierre-Marie Pédrot | |
| 2014-03-01 | Fixing bad comparison in Detyping. | Pierre-Marie Pédrot | |
| 2014-02-28 | Removing Pervasives.compare in Termdn. | Pierre-Marie Pédrot | |
| 2014-02-28 | Removing a Pervasives.compare in Term_dnet. | Pierre-Marie Pédrot | |
| 2014-02-28 | Fix bug 3245: 'simpl nomatch' argument annotation makes cbn go into an ↵ | Pierre Boutillier | |
| infinite loop. | |||
| 2014-02-28 | Dead code elimionation in reductionops | Pierre Boutillier | |
| 2014-02-27 | Tacinterp: refactoring using Monad. | Arnaud Spiwack | |
| Adds a combinator List.map_right which chains effects from right to left. | |||
| 2014-02-27 | Code refactoring thanks to the new Monad module. | Arnaud Spiwack | |
| 2014-02-26 | remoteCounter: backup/restore | Enrico Tassi | |
| When you resume the compilation of a .vi file, you want to avoid collisions on fresh names. | |||
| 2014-02-24 | IStream: change type of thunk, spare allocations. | Arnaud Spiwack | |
| Two changes: - 'a Lazy.t becomes unit -> 'a - 'a t becomes 'a u (the view type) This spares two Lazy.force, and leverages Lazy.lazy_from_fun. Considering Lazy.force is fairly slow, in particular because of the write-barrier, this should be beneficial. | |||
| 2014-02-24 | Ensuring that the module Stack is opaque inside Reductionops. | Pierre-Marie Pédrot | |
| 2014-02-24 | cbn understands Arguments | Pierre Boutillier | |
| (excepts list of args that must be constructors | |||
| 2014-02-24 | Simpl_behaviour becomes Reductionops.ReductionBehaviour | Pierre Boutillier | |
| syntax mentionning simpl remains | |||
| 2014-02-24 | Create Debug Unification option | Pierre Boutillier | |
| to dump states that Evarconv.eq_appr_x tries to unify. | |||
| 2014-02-24 | No more translation array <-> list in Reductionops.Stack | Pierre Boutillier | |
| 2014-02-24 | Reductionops.Stack.strip* are ready to deal with Shift | Pierre Boutillier | |
| 2014-02-24 | Reductionops.Stack.app_node is secret | Pierre Boutillier | |
| 2014-02-24 | app_node, stack, state printers | Pierre Boutillier | |
| 2014-02-24 | Stack operations of Reductionops in Reductionops.Stack | Pierre Boutillier | |
| 2014-02-12 | TC: honor the use_typeclasses flag in pretyping | Enrico Tassi | |
| The coercion code was not seeing such flag and always trying to resolve type classes. In particular open_contr is pretyped without type classes. | |||
| 2014-02-11 | Made Pre_env.lazy_val opaque. | Pierre-Marie Pédrot | |
| 2014-02-03 | Tracking memory misallocation by trying to improve sharing. | Pierre-Marie Pédrot | |
| 2014-01-29 | Using Map.smartmap whenever deemed useful. | Pierre-Marie Pédrot | |
| 2014-01-27 | Abstracting away coercion indexes in Classops. | Pierre-Marie Pédrot | |
| 2014-01-26 | Coercions: avoid imperative data structure | Enrico Tassi | |
| 2014-01-07 | STM: additional fix for STM + vm_compute | Enrico Tassi | |
| Thanks again Maximes. This time the C value was stored in the env_(named|rel)_val of the environment | |||
| 2013-12-30 | When resetting an evarmap with the unsafe function Evd.evars_reset_evd with | Pierre-Marie Pédrot | |
| the flag with_conv_pbs, only reset the metas, not the last_mod field. It seemed strange to mix two unrelated things. This did not break anything visible... | |||
| 2013-12-30 | Support for evars and metas in native compiler. | Maxime Dénès | |
| Experimental. Turned out to be much harder to implement than I thought. The main issue is that the reification in the native compiler and the VM is not quite untyped. Indeed, type annotations for lambdas have to be reconstructed. Hence, when reifying an application u = t a1 ... an, the type of t has to be known or reconstructed. It is always possible to do so in plain CIC, when u is in normal form and its type is known. However, with partial terms this may no longer be the case, as in: ?1 a1 ... an. So we also compile and evaluate the type of evars and metas. This still has to be tested more extensively, but the correction of the kernel native conversion (on terms without evars or metas) should not be impacted. Much of this could be reused for the VM. | |||
| 2013-12-06 | Fix test-suite/success/evars.v. | Arnaud Spiwack | |
| In commit a92a27 (Fix the compilation of pattern matching wrt to variables), I introduced a serious bug in which, in some case, the infered return predicate of a pattern matching would be lifted wrongly. Because I wrote [false] instead of [true] at one location (which prevented creation of aliases and so created shorter named_context than expected). | |||
| 2013-12-03 | Removing useless meta-related functions. | Pierre-Marie Pédrot | |
| 2013-11-30 | Better heuristic for name generation backward compatibility. We fallback | Pierre-Marie Pédrot | |
| to old behaviour whenever we were in Program mode. | |||
| 2013-11-30 | Useless instantiation function exported in Evd. | Pierre-Marie Pédrot | |
| 2013-11-30 | Tentative fix to recover fresh name generation as it was before | Pierre-Marie Pédrot | |
| new-tacticals merge. This is essentially a revert of 6fea2f which broke the sacrosanct backward compatibility of name generation, thus breaking quite a lot of contribs. | |||
| 2013-11-27 | Adding generic solvers to term holes. For now, no resolution mechanism nor | Pierre-Marie Pédrot | |
| parsing is plugged. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |