aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Fix interface for template polymorphism, cleaning up code in all typing algor...Gravatar Matthieu Sozeau2014-05-06
* Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.Gravatar Matthieu Sozeau2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Fixing #3293 (eta-expansion at "match" printing time was failingGravatar Hugo Herbelin2014-04-28
* Adding a field ci_cstr_nargs to case_info and mind_consnrealargs toGravatar Hugo Herbelin2014-04-28
* Fix a second, trickier, typo in Termops.eta_reduce_head.Gravatar Arnaud Spiwack2014-04-25
* Fix a small typo in Termops.eta_reduce_head.Gravatar Arnaud Spiwack2014-04-25
* Better representation of evar filters: we represent the vacuous filters ofGravatar Pierre-Marie Pédrot2014-04-23
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Readback for int31 values from native compiler.Gravatar Maxime Dénès2014-04-09
* Fixing bug #3228 (fixing precedence of ltac variables over variables in env).Gravatar Hugo Herbelin2014-04-05
* Fixing #3262 which revealed a non-progressing, hence looping,Gravatar Hugo Herbelin2014-04-04
* Propagating conversion_problem towards (postponed) evar/evar problems.Gravatar Hugo Herbelin2014-04-01
* Fixing bug #2900 (evar/evar unif was supposed to be treated inGravatar Hugo Herbelin2014-04-01
* Evarconv: exact_ise_stack looks to stack head before bodies or branchesGravatar Pierre Boutillier2014-03-17
* consider_remaining_unif_problems respects Conv_oracleGravatar Pierre Boutillier2014-03-16
* Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it hadGravatar Pierre-Marie Pédrot2014-03-14
* Evarconv unification respects Conv_oracleGravatar Pierre Boutillier2014-03-10
* MaybeFlexible semantic changesGravatar Pierre Boutillier2014-03-10
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Goptions do not rely anymore on generic equality.Gravatar Pierre-Marie Pédrot2014-03-03
* Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Gravatar Pierre Letouzey2014-03-02
* Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codeGravatar Pierre Letouzey2014-03-02
* Adding an equality function over glob_constrGravatar Pierre-Marie Pédrot2014-03-02
* Fixing pervasive comparisonsGravatar Pierre-Marie Pédrot2014-03-01
* Fixing bad comparison in Detyping.Gravatar Pierre-Marie Pédrot2014-03-01
* Removing Pervasives.compare in Termdn.Gravatar Pierre-Marie Pédrot2014-02-28
* Removing a Pervasives.compare in Term_dnet.Gravatar Pierre-Marie Pédrot2014-02-28
* Fix bug 3245: 'simpl nomatch' argument annotation makes cbn go into an infini...Gravatar Pierre Boutillier2014-02-28
* Dead code elimionation in reductionopsGravatar Pierre Boutillier2014-02-28
* Tacinterp: refactoring using Monad.Gravatar Arnaud Spiwack2014-02-27
* Code refactoring thanks to the new Monad module.Gravatar Arnaud Spiwack2014-02-27
* remoteCounter: backup/restoreGravatar Enrico Tassi2014-02-26
* IStream: change type of thunk, spare allocations.Gravatar Arnaud Spiwack2014-02-24
* Ensuring that the module Stack is opaque inside Reductionops.Gravatar Pierre-Marie Pédrot2014-02-24
* cbn understands ArgumentsGravatar Pierre Boutillier2014-02-24
* Simpl_behaviour becomes Reductionops.ReductionBehaviourGravatar Pierre Boutillier2014-02-24
* Create Debug Unification optionGravatar Pierre Boutillier2014-02-24
* No more translation array <-> list in Reductionops.StackGravatar Pierre Boutillier2014-02-24
* Reductionops.Stack.strip* are ready to deal with ShiftGravatar Pierre Boutillier2014-02-24
* Reductionops.Stack.app_node is secretGravatar Pierre Boutillier2014-02-24
* app_node, stack, state printersGravatar Pierre Boutillier2014-02-24
* Stack operations of Reductionops in Reductionops.StackGravatar Pierre Boutillier2014-02-24
* TC: honor the use_typeclasses flag in pretypingGravatar Enrico Tassi2014-02-12
* Made Pre_env.lazy_val opaque.Gravatar Pierre-Marie Pédrot2014-02-11
* Tracking memory misallocation by trying to improve sharing.Gravatar Pierre-Marie Pédrot2014-02-03
* Using Map.smartmap whenever deemed useful.Gravatar Pierre-Marie Pédrot2014-01-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 07:01:32 +0000